Vision

Logos is a systems programming language in which everything lives in one structure, the Logic Graph: the program, its types and proofs, the compilation rules and optimization passes, the compiler itself, the documentation, and the language's own parsing rules. The language reads, checks and rewrites that structure, so there is no separation between "the language" and "what is written in it." That single commitment is radical unification.

The bet is that the boundaries we take for granted (language versus compiler, code versus specification, program versus proof, source versus tooling) are accidents of how systems were historically built, not necessities. Collapse them and what is left is simpler at its core, more expressive in what it can state, and more honest about what it is.

Why now: machines write the code

The unification idea is old. A reflective, rewritable structure that carries its own types and proofs was a luxury while humans wrote code, which is part of why its closest ancestors stayed niche. When models write most code it becomes a requirement. A model editing text pushes a guess through a fragile toolchain and hopes. A model editing the Logic Graph rewrites a structure that already carries scopes, types, borrow states and proofs, and gets machine-checked feedback that the change is correct and safe before it runs. A non-human author most needs machine-checked correctness and least reliably supplies it.

The target is the union of Smalltalk and Lean on a systems base: rewrite as freely as Smalltalk, check as strictly as Lean, run as fast as Rust, in one structure. The claim is testable. As soon as the preview exists, a model given the graph and its checked feedback is measured against the same model on an established text language.

One structure, all the way down

The Logic Graph is the primary representation. It holds the program with every piece of semantic information attached (resolved scopes, inferred types, borrow states, propagated capabilities), the rules that governed its parsing, the standard library, and the compiler's own logic. Navigation is uniform: the same operations you run on your own code traverse any subgraph, including the compiler's.

One cell, one evaluation rule

Every node in the graph is a dyad: a pointer to a type and a pointer to a value, sixteen bytes. The type says how the value is read, and following type pointers always ends at type, whose type is itself. To evaluate a dyad, read its type: if it is a function, run it on the value; if it carries a run body, run that over the node's fields; otherwise the dyad is data. Operators, field access and if are all functions, and operands arrive unevaluated, so if runs only the branch it takes without being a special form.

A function is a type in that same shape, and so is an operator: ^ := type (…) declares its operands as fields and fills its parse_rank, its associativity, a parse that builds the node from the cells around it, and a run that computes it. The parser is in the graph. There is no grammar file, and defining new syntax is writing a type.

One pass

Source becomes graph one token at a time, and each expression runs as soon as it is built. Lexing, parsing and running interleave in one pass, so compile-time evaluation is ordinary interpretation that happens earlier: a function can return a type, a declaration can take the type it computed, and an if whose condition is known drops the untaken branch before it is parsed. Comptime runs without I/O, so a build is a pure function of its source. There is no main: the top level is the program, and everything after logos on the command line is one line of Logos source. The binary has no subcommands and no compile flags; what compiles, links and builds is decided inside the source.

A tiny seed that self-hosts

A small Rust bootstrap seed starts the system: a parser producing graph nodes, an evaluator for them, enough type machinery to check the kernel, a path to Cranelift. Everything beyond, the full type system, the borrow checker, the rewriting engine, the optimization passes, the standard library, is written in Logos and processed by the seed until the system compiles itself. The seed ships every primitive as native, callable machine code with no Logos source, and self-hosting replaces them with Logos one at a time; the set shrinks toward a floor that can never have source, such as allocation and syscalls. The seed stays small enough to audit by hand, and eventually to verify.

Interpret by default, compile on demand

Logic Graph code is interpreted by default. Write compile f and the function is JIT-compiled with Cranelift: the next call jumps to machine code, and the compiled function stays fully reflectable through the graph it came from. Any function can be compiled, mutable code included; a structural edit to compiled code drops the compiled form and falls back to interpretation. Because interpreting and compiling produce the same result, the choice is only ever about whether the speedup is worth the cost of compiling, never about what the code means.

Memory safety without a garbage collector

Logos is a serious systems language. Memory is managed by a borrow checker with lexical lifetimes, explicit ownership, and moves, with no garbage collector and no runtime cost. One rule covers every case: among references that are live at the same time and overlap, there may be many readers or a single writer, never both. Borrows are tracked per place, a field, an element, a predicate-defined set of indices, so exclusive and shared borrows of disjoint parts coexist.

Nothing is destroyed behind your back

Locals live on the stack and go away with their scope. The heap is explicit: alloc n of T v returns an owning pointer and writes its own teardown, defer free, into the scope that owns it, as ordinary graph structure that reflection can read. Any constructor may do the same, and a type whose fields carry teardowns must write its own drop. own x moves ownership and ends the name on that line; drop x runs the destructor now. Both are decided at parse, so a use after a move is refused before anything runs, and there is no run-time drop flag. Because teardown is structure rather than hidden glue, "every alloc reaches a free on every path" is a fact the proof layer can prove over the graph.

Gates: one rule for read and write

Visibility, mutability, borrowing and reflection are one primitive: a read or write capability over a place, granted to a scope. A declared name is private and immutable unless its declaration says otherwise. pub widens reading, mut allows writing, immut takes it back, lock seals the set for good, and share marks one place stored once with a type or a function instead of once per value. Gates are fail-closed predicates: only an explicit true permits, and an unknown stays visible as an obligation a later proof can discharge. Access is decided lexically at elaboration, never looked up by running code, so being called by a holder grants nothing. There is no shadowing anywhere.

Errors are values

A fallible function returns T!, the value or an error, and its caller handles it with match or passes it on with try: one visible word per call site, no exceptions, no hidden propagation. Every error names a category declared in a scope, error.not_found «…», so two libraries' categories never collide, and the error value carries one element per hop from the raise to the handler, each with its exact graph location and an optional value. A broken invariant is not an error but a fault: abort «…» cancels the task, its pending teardowns run, and the diagnostic is the reason.

One rewriting engine

Compiler optimization, computer algebra, and your own transformations are one operation: take a fragment, apply rewrite rules, and extract the form that minimizes a cost function, using equality saturation over an e-graph. The same engine serves the compiler's x + 0 → x and the mathematician's sin²(θ) + cos²(θ) → 1.

Proofs are rewrite rules

A systems programmer gets the base type system and a borrow checker. Beyond that the strata are opt-in: refinement types and pre/post-conditions discharged by an SMT solver, then termination measures, then proofs, and parts of a program can be verified while the rest stays lower. A proof is written as mathematics is: double := conjecture ( a + a == 2 * a ) where ( a:type is number ) states a boolean over holes, and calling it, double(x + x), yields the other side of the fact. A derivation is a chain of relations, each step citing its rule, checked by a small trusted core that demands totality. Because a rule is its own proof, simplification provably preserves what it rewrites, and a verified computer algebra system comes out as a library. Every proof carries the set of axioms it rests on, so contradictory theories coexist in one graph and combine only where their union stays consistent.

Capabilities are positions, not modes

A section is a region of code defined by which names reach it, and the root section, the arche, is the scope a run starts in. The effect identities, files, network, clock, environment and extern, the door out of the graph, reach a section only as references deliberately handed down, so what a dependency can do is read off what it was given. Pure computation is ambient. An effectful program's invocation names its authority, logos import ./app.logos, main(fs): the shell line is the grant, visible in history. Nothing asks "which mode am I in"; there is only what a scope can name.

Concurrency the compiler checks

Two shapes cover the common cases. parallel for distributes work over disjoint indices, a pattern the borrow checker recognizes and proves race-free; stackless async tasks handle I/O-bound concurrency on executor pools you control, pausing only at an explicit .await so suspension is always visible in the source. Reading shared graph structure across threads is an ordinary shared borrow, so the standard library and every definition can be read by many threads at once, while writes are exclusive and concurrent mutation of the same node is a compile-time error.

Languages inside the language

A grammar is data, so a language is a type: language (…) opens a closed section holding five names, and every other word it uses is declared, fetched from Logos through the door logos (…) or given a meaning of its own. A constructor's parse is unrestricted code, so surfaces as irregular as natural language are in scope: hosted text parses to data, ambiguity is represented rather than searched, and a sentence denotes a proposition the proof layer checks. Englogos, a regular human language whose grammar is Logic Graph constructors from the start, is the far-horizon direction on the same substrate.

The compiler is a library

Above the seed, the borrow checker, type checker, rewriting engine, optimization passes, and the lowerings from Logic Graph to native code are themselves Logos programs and themselves subgraphs. Adding an optimization is library work; targeting a new platform is implementing the backend interface and contributing rules. The grammar lives in the graph too, so a new operator, constructor, or macro is ordinary library work rather than a change to the language itself.

The tooling is Logos too

Because so much is already in the Logic Graph, the tooling is thinner and richer than its equivalents elsewhere. A Logos-written language server brings highlighting, errors, autocomplete, go-to-definition, and refactoring to any LSP editor; the documentation generator works from the same graph that holds types, signatures, examples, capabilities, and proofs; and a structural editor that operates directly on Logic Graphs is the long-term goal. The Smalltalk vision of a fully malleable system, applied to a modern systems language.

What ships when

Versions are named vX.Y.Z. What runs today is the bootstrap seed, a small Rust program that turns Logos source into the Logic Graph, interprets it, and compiles the functions you ask it to. v0.1.0 is the preview and the first public milestone, built to show the language defining itself: a power operator written in ordinary Logos, used in the same file and compiled with compile f. Error values, pub and mut are in it; the borrow checker, the rewriting engine and verification come after. v1.0.0 is the release and the stability promise. The standard library and the proof layer ship inside it, because a minimal core whose gaps are filled downstream is how languages fragment.