One language for everything: Logos aims to be a single language for systems code, speed, GPUs, async, proofs, metaprogramming, new languages, dedicated hardware, and its own compiler, instead of a different one for every job.

An AI that edits text pushes a guess through a fragile toolchain and hopes. Logos code is a live structure that carries its own types, borrow states, and proofs, so every change gets machine-checked feedback before it ever runs.

Read the vision See the roadmap

In principio erat Verbum, et Verbum erat apud Deum, et Deus erat Verbum.

- John 1:1

τοῦ δὲ λόγου τοῦδ’ ἐόντος αἰεὶ ἀξύνετοι γίνονται ἄνθρωποι καὶ πρόσθεν ἢ ἀκούσασι καὶ ἀκούσαντες τὸ πρῶτον.

- Heraclitus

λόγος δυνάστης μέγας ἐστίν, ὃς σμικροτάτῳ σώματι καὶ ἀφανεστάτῳ θειότατα ἔργα ἀποτελεῖ.

- Gorgias

Non igitur constat pluribus verbis, sed est unum Verbum per quod facta sunt omnia.

- Anselm

λόγον δὲ μόνον ἄνθρωπος ἔχει τῶν ζῴων… ὁ δὲ λόγος ἐπὶ τῷ δηλοῦν ἐστι τὸ συμφέρον καὶ τὸ βλαβερόν, ὥστε καὶ τὸ δίκαιον καὶ τὸ ἄδικον

- Aristotle

Eius autem vinculum est ratio et oratio.

- Cicero

ψυχῆς πείρατα ἰὼν οὐκ ἂν ἐξεύροιο, πᾶσαν ἐπιπορευόμενος ὁδόν· οὕτω βαθὺν λόγον ἔχει.

- Heraclitus

διάνοια μὲν καὶ λόγος ταὐτόν· πλὴν ὁ μὲν ἐντὸς τῆς ψυχῆς πρὸς αὑτὴν διάλογος ἄνευ φωνῆς γιγνόμενος.

- Plato

Oratio vultus animi est.

- Seneca

λόγος ἀληθὴς καὶ νόμιμος καὶ δίκαιος ψυχῆς ἀγαθῆς καὶ πιστῆς εἴδωλόν ἐστι.

- Isocrates

Deus uno actu et se et omnia intelligit, unicum Verbum eius est expressivum non solum Patris, sed etiam creaturarum.

- Thomas Aquinas

ὁ δὲ τοῦ θεοῦ λόγος ἐστὶν ὁ δεσμός τῶν πάντων, συνέχων τὰ μέρη καὶ σφίγγων.

- Philo of Alexandria

ψυχῆς ἐστι λόγος ἑαυτὸν αὔξων.

- Heraclitus

Sermo datur cunctis, animi sapientia paucis.

- Disticha Catonis

ζῶν γὰρ ὁ λόγος τοῦ θεοῦ καὶ ἐνεργὴς καὶ τομώτερος ὑπὲρ πᾶσαν μάχαιραν δίστομον.

- Hebrews 4:12

Verba volant, scripta manent.

- Latin proverb

ὁ δὲ θεὸς οὐδὲν ἄλλο ἐστὶν ἢ νοῦς καὶ λόγος.

- Stoic tradition

What Logos looks like

Target syntax, taken straight from the language design and the docs: everyday systems code and the language's own definition live in the same structure. The compiler that runs it is still being built; the roadmap tracks what actually works today.

target-syntax.logostarget syntax, not yet runnable

# Declare with `:=`, reassign with `=`. `mut` marks a mutable value.
count := mut i32 0
count = count + 1

# Systems code: borrowed references, checked errors, no GC.
advance := fn (tokens : &mut array synolon, idx : u64) -> void! (
    if idx+1 >= tokens.size
        error «not enough tokens after idx»
)

# The language is written in itself. A node (a synolon) is two slots,
# logos and hyle, and even `+` is an ordinary identity: a node carrying
# a precedence and the code for how it reads its operands. There is no
# separate macro language, so new syntax is just more declarations in
# the same graph.
synolon := logos (logos := @synolon ?, hyle := @void ?)
+ := logos (
    shared precedence    := f64 6.0
    shared associativity := u8 left_to_right
    shared constructor   := fn (tokens : &mut array synolon, idx : u64) -> void! ( ? )
)

The program is the structure

Radical unification is not a metaphor. The smallest program, a = a + 1, is not text a compiler reads once and throws away. It is a graph, the Logic Graph (LG), named because it should be able to hold any logic imaginable. And because it is a graph, the same structure can reflect on itself, interpret itself, or compile and run itself.

a = a + 1

becomes

Read it left to right: every arrow leaves one field of a node (the :@synolon or :@void next to it is what that field points at) and points at another whole node. A synolon is a node of exactly two slots: a logos, which says what the node is, and a hyle, the matter the logos gives meaning to. Here each hyle points at an operand record whose fields (lhs, rhs) are defined by the logos. So a = a + 1 unfolds into synolons and operand records, bottoming out at the identities =, +, rational_number, the variable a, and the literal 1. Both lhs fields point at the one a, so it is genuinely a graph, not a tree. Because your program already is this structure, the same operations that run it can read it, rewrite it, optimize it, and prove it, so the optimizer, the computer-algebra system, the proof checker, and metaprogramming are one thing over one structure rather than four tools bolted on from outside.

Why one structure, and why now

When people wrote all the code, a structure that carries its own types and proofs and can rewrite itself was a luxury. When models write most of it, that same structure becomes the requirement.

An AI that edits text pushes a guess through a fragile toolchain and hopes it holds. An AI that edits a Logic Graph rewrites a structure that already carries its scopes, types, borrow states, and proofs, and gets machine-checked feedback that the change is correct and safe before it ever runs. The same reader-writer rule that governs memory also governs self-modifying code, so a program can improve its own code, iteratively, without being allowed to break it.

This is the gap between the two systems Logos learns from. Smalltalk gave a live system that can inspect and rewrite itself, but nothing that could prove a change was right. Lean gives machine-checked proof, but it is a prover built for mathematicians, garbage-collected and functional, not a systems substrate a program rewrites and runs at native speed. Neither has both halves. Logos reaches for both in one structure: rewrite it as freely as Smalltalk, check it as strictly as Lean, run it as fast as Rust.

That combination is what code written by machines will need, and it is the direction Logos is built toward. It does not run yet; the roadmap tracks what does.

Built from proven parts

Logos is large, and honest about being large. But none of its parts is without precedent: self-hosting (Lean 4), a layered intermediate representation (MLIR), equality saturation in production (egg and Cranelift), borrow checking without a garbage collector (Rust), a live and malleable system (Smalltalk), machine-checked proofs (Lean). The novel work is uniting them in one structure, not inventing any one of them.

The path is a small Rust seed, kept small enough to audit by hand. Everything above it is written in Logos, until the language compiles itself: a tiny trusted core, and then the language builds the rest. The roadmap breaks the work into parts and shows what already runs, and the vision shows how each hard part is solved.

Next to its neighbors

The first question a language-literate visitor asks is "why not C++, Rust, Zig, Lean, Julia, Python, TypeScript, or a Lisp?". Here is the honest answer. Logos is not done yet: its column is the design it is being built toward, not software you can run today, while every other column is what ships now. But read across the rows: nearly every capability in the Logos column is already a yes somewhere else here, so the hard part is not inventing any one of them, it is uniting them in one structure. Some rows are things other languages do well that Logos does not attempt at all.

has it
partial
no

Capability	Logos	C/C++	Rust	Zig	Lean 4	Unison	Racket	Smalltalk	Julia	Python	TS/JS	Mojo
Memory safety without a GCownership and borrow checking, zero runtime cost	yes	no¹⁶	yes	no⁹	no	no	no	no	no	no	no	partial¹³
Compiles to native machine codeAOT or JIT, systems-grade performance	yes	yes	yes	yes	yes¹	partial	partial	partial	yes	partial¹⁸	partial	yes
The speed ceiling of C and Rustno GC or boxing tax, zero-cost abstractions	yes	yes	yes	yes	no¹	no	no	no	partial²¹	no	no	yes
Targets GPUs and custom hardwarekernels written in the language itself, not shader strings	yes	yes	partial¹¹	partial	no	no	no	no	yes	partial¹⁹	no	yes
Runs in the browsercompiles to WebAssembly or runs in a web page	partial³²	partial³²	partial³²	partial³²	no	no	no	partial²⁷	no	partial²⁸	yes	no
Multithreaded parallelismuse every core with shared memory	yes	yes	yes	yes	partial	partial	partial	no	yes	partial²⁰	partial	yes
Async concurrencyasync/await or lightweight tasks for IO-bound work	yes	partial²⁵	yes	partial²⁶	partial	yes	yes	partial	yes	yes	yes	partial
Formal proofs in the languagedependent types / theorem proving built in	yes	no	no	no	yes	no	no	no	no	no	no	no
Gradual verificationprove one part, leave the rest ordinary code	yes	no	no	no	yes	no	no	no	no	no	no	no
Effects tracked in typespurity, IO, async as capabilities the compiler checks	yes	no	partial	no	yes	yes	no	no	no	no	no	partial
Code as dataprograms are a structure the language can read	yes	no	partial²	no	yes	partial	yes	yes	yes	yes	partial	no
Semantic reflectionthe readable structure carries types and checked facts	yes	partial¹⁷	no	partial	yes	no	partial	partial³	partial	partial	partial²⁹	no
Compile-time code executionrun ordinary code at compile time, results baked in	yes	partial	partial	yes	yes	no	yes	partial¹⁵	yes	no	no	yes
Compiler extensible as a librarynew syntax and optimizations as ordinary libraries	yes	no	partial²	no	yes	no	yes⁴	yes	partial	no	partial	no
Hosts other languages as librariesembed an HDL or shader language without a new compiler	yes	no	partial	partial	yes¹⁴	no	yes⁴	no	partial	no	partial	no
Hygienic syntax extensionsyntax extensions can't capture names by accident	yes²²	no	partial	no	yes	no	yes	no	yes	no	no	no
First-class rewrite engineequality saturation shared by compiler and user code	yes	no	no	no	partial⁵	no	partial⁸	partial⁸	no¹²	no	no	no
Live systemredefine parts of a running program	yes	no	no	no	no	partial	partial	yes	yes	partial	partial	no
Image persistencesave the whole running system, resume it later	partial²³	no	no	no	no	no	no	yes	partial²⁴	no	no	no
Content-addressed codedefinitions identified by hash of their content	partial⁶	no	no	no	no	yes	no	no	no	no	no	no
Usable todaya stable compiler you can build real software on now	no	yes	yes	partial¹⁰	yes	yes⁷	yes	yes	yes	yes	yes	partial¹³
Backward-compatibility promisecode from years ago still builds and runs today	partial³⁰	yes	yes	no¹⁰	partial	partial	yes	partial	yes	partial	yes	no
Package ecosystempackages, users, production track record	partial³¹	yes	yes	partial	partial	partial⁷	partial	partial	yes	yes	yes	no

Lean 4 compiles through C, but its runtime uses reference counting: fast, yet not a no-GC systems language.
Rust proc macros transform token streams before type checking; the compiler's passes are not extensible.
Smalltalk reflects everything at runtime, but nothing is statically typed or proved.
Racket's #lang makes whole languages ordinary libraries; the optimizer itself is not user-extensible.
Lean's simp and @[csimp] rule sets are first-class directed rewriting; there is no e-graph equality saturation.
Logos source files stay canonical, but hash identity can be enforced as an opt-in wrapper discipline: persisted artifacts already key by content, never by address.
Most of Unison's public production mileage is Unison Cloud, built by the language's own company.
Racket's macro expander and Smalltalk's Refactoring-Browser rewriter are user-drivable tree rewriting; neither is equality saturation, and neither serves as the compiler's optimizer.
Zig has no GC, but its safety comes from runtime checks in safe builds, not compile-time proof.
Zig is pre-1.0 by design; Bun, TigerBeetle, and Ghostty ship on it in production anyway.
Rust reaches GPUs through rust-gpu (SPIR-V) and the tier-2 nvptx64 target; every path is still experimental.
Metatheory.jl gives Julia real e-graph rewriting as a library, but the compiler itself never uses it.
Mojo's 1.0 beta shipped in May 2026 with ownership checking working today; full default memory safety is deferred to Mojo 2.x.
Alloy embeds real C syntax inside Lean files through Lean's extensible grammar.
Smalltalk has no separate compile phase; evaluating code and saving the image plays the comptime role.
C and C++ have no GC, but nothing enforces memory safety either; this row asks for both.
C++26 adds compile-time reflection of types (P2996), not reflection of program structure.
CPython 3.13+ ships an experimental JIT and PyPy is mature; neither approaches systems-grade performance.
Triton and JAX compile Python-syntax kernels for GPUs, as restricted subsets of the language.
Free-threaded CPython became officially supported in Python 3.14, as a separate build; the default build keeps the GIL.
Type-stable Julia kernels reach C speed; the GC and dynamic fallback keep whole programs below the ceiling.
Logos constructors emit resolved handles rather than names, so there is no name for a macro to capture.
The Logic Graph and boundary-materialized task state admit a save/resume library in Logos; source files stay the canonical form.
PackageCompiler sysimages snapshot a loaded Julia session, not live tasks.
C++20 has coroutines but no standard async runtime; std::execution only arrives with C++26.
Zig dropped its old async/await in the compiler rewrite; a new std.Io async design is landing across 0.x releases.
SqueakJS runs real Smalltalk images in the browser on a JavaScript virtual machine.
Pyodide runs CPython on WebAssembly; C-extension packages need prebuilt WASM wheels.
The TypeScript compiler API exposes the type checker to tooling; all types are erased at runtime.
Logos releases are designed immutable from day one (docs and builds freeze per version); the track record starts at the first release.
No Logos packages exist yet; the standard library is deliberately built before release to seed a coherent ecosystem.
WebAssembly runs in every browser, but only JavaScript runs alone: wasm still needs JS glue to load, and all DOM and I/O access goes through JS.

What Logos looks like

The program is the structure

Why one structure, and why now

Built from proven parts

Next to its neighbors

Hear about the first build