Λόγος
Download

Roadmap

The headline is the destination, not the current release. Logos is pre-alpha and nothing here ships yet. Everything above the v1 interchange is in progress now; everything below it is planned, landing across later versions.

v0bootstrap begins

The Logic Graph

  1. One structure for everything

    The Logic Graph: one structure holding programs, types, the standard library, and the compiler's own logic, all traversed by the same operations.

    In progress

  2. A tiny seed that self-hosts

    A minimal Rust seed bootstraps the system and processes Logos until it compiles itself; its primitives ship as opaque native code and are ported to reflectable Logos source over time.

    In progress

  3. The mutability and construction model

    mut as a recursive type modifier and an undefined-to-defined-to-frozen lifecycle, so immutability is the default and frozen is final.

    In progress

  4. Source and runtime graphs

    A persistent file-backed source graph that is the program's identity, plus an ephemeral arena-allocated runtime graph cleaned up by scope lifetimes, no GC.

    In progress

Parsing & identity

  1. Syntax is data

    The grammar lives in the graph, so a new operator, constructor, or macro is ordinary library work rather than a change to the language.

    In progress

Execution

  1. Interpret by default, JIT on demand

    Logic Graph code is interpreted directly; a frozen region JIT-compiles via Cranelift and stays reflectable through the graph it came from. Hot regions are promoted to native code automatically and deoptimized back to in…

    In progress

  2. Compile-time evaluation and metaprogramming

    A comptime marker bakes results into the artifact, with the whole language available at parse time over real Logic Graph rather than a macro sublanguage.

    In progress

Compilation & optimization

  1. The compiler is a library

    The checker, optimizer, and the lowerings to native code are ordinary Logos over the graph, not a sealed black box.

    In progress

  2. One rewriting engine

    A single equality-saturation engine for compiler optimization, computer algebra, and user transforms, with first-class rule sets and cost functions.

    In progress

  3. The Logos IR

    A target-agnostic intermediate layer with explicit basic blocks, control flow, memory operations, and types, itself a stratum of the graph. One backend interface consumes it, so Cranelift (the default), LLVM, and other…

    In progress

Memory & concurrency

  1. User-replaceable allocators

    Arena, bump, pool, system, and custom allocators behind one interface, with arenas carrying the graph's cyclic structures.

    In progress

  2. Multithreading and task scheduling

    Two concurrency shapes the borrow checker proves race-free. parallel for spreads work over disjoint indices, with threads reading shared graph structure through ordinary shared borrows while writes stay exclusive. Stack…

    In progress

Interop & errors

  1. Errors are values

    Fallible functions return tagged unions (T | Error), handled explicitly via match; no exceptions and no implicit propagation in the core.

    In progress

  2. Native interop and the Rust bridge

    Calling existing native code in-process across the C ABI with no linker step, independent of which backend compiled either side.

    In progress
v1first self-hosting release

Parsing & identity

  1. The identity-recognition engine

    One engine for parsing, reflection, and rewrite matching: a merged, stratified recognizer that returns every identity matching at a node.

    Planned

  2. Incremental re-identification

    Edits touch only the tokens they change; each cached identity is a reader, invalidated exactly when the tokens or rules it consulted change.

    Planned

Memory & concurrency

  1. The borrow checker, one read/write rule

    Lexical lifetimes, ownership, and moves with no GC; place- and reference-granular borrows; the same many-readers-or-one-writer rule that also governs visibility and reflection.

    Planned

Types & proofs

  1. Capability and effect tracking

    Effects as capabilities (pure, total, async, thread-pinned, GPU-subset, allocator-bound) tracked through the call graph, so compile-time code is I/O-free and builds reproduce.

    Planned

  2. Pay only for what you verify

    Opt-in strata: refinement types with SMT discharge, then pre- and post-conditions, then termination measures. Lower code is never burdened by higher guarantees.

    Planned

  3. Dependent types and a proof kernel

    Propositions as types and proofs as programs, checked by a small trusted kernel and erased before codegen, with a stratified universe hierarchy.

    Planned

  4. The ecumenical proof system

    Many theories in one graph, including contradictory ones, each proof carrying the axioms it rests on so that only consistent results combine.

    Planned

Tooling

  1. A batteries-included standard library

    Single canonical solutions decided and documented before release: collections, strings, numerics, symbolic math, allocators, concurrency, I/O, and verification.

    Planned

  2. LSP-first editor support

    A Logos-written language server bringing rich highlighting, errors, autocomplete, and refactoring to any LSP editor.

    Planned

  3. Debugger and profiler integration

    Standard-protocol DAP debugging, samplers, and flamegraphs, so users keep the tools they already know.

    Planned

  4. A documentation generator

    Generated from the same graph that holds types, examples, capabilities, and proofs, so docs carry verified examples and proof obligations.

    Planned

  5. A Logos-native structural editor

    Semantic editing directly on Logic Graphs and an IDE customizable in Logos: the long-term goal, not on the critical path.

    Planned

Branch lines release across v1.X · v2 · v3.