One structure for everything
Programs, types, proofs, the optimizer, the standard library, even the compiler's own logic live in a single reflectable structure. The same operations you run on your code traverse any of it.
One idea, all the way down
A tiny seed that self-hosts
A minimal Rust seed starts the system; everything beyond is written in Logos until it compiles itself. Small enough to audit by hand, and eventually verify.
Interpret by default, JIT on demand
Code is interpreted by default; freeze a region and it JIT-compiles via Cranelift, staying fully reflectable through the graph it came from.
Memory safety without a garbage collector
A borrow checker with lexical lifetimes, ownership, and moves: many readers or one writer, proven at compile time. No garbage collector, no runtime cost. The same rule governs visibility, borrowing, and reflection alike.
One rewriting engine
Compiler optimization, computer algebra, and your own transforms are one operation. The same engine serves x + 0 → x and sin²θ + cos²θ → 1.
Pay only for what you verify
Memory safety comes free; above it, opt-in refinement types, pre- and post-conditions, then full dependent-type proofs checked by a small kernel. Lower code is never burdened by higher guarantees.
The compiler is a library
The borrow checker, type checker, optimizer, and the lowerings to native code are ordinary Logos over the graph, not a sealed black box. Adding an optimization or a backend is library work.
Concurrency without data races
parallel for over disjoint indices and stackless async tasks, with the borrow checker proving data-race freedom statically. Shared graph reads are free; writes are exclusive.
Never settle for "ok" syntax
Syntax is data too. The grammar lives in the graph, so the language can be extended and rewritten: a constructor or macro is ordinary library work.