The compiler that
compiles itself.
souc is written in Sounio. Bootstrap starts with a C-compiled seed binary, runs through three stages, and terminates when Stage 2 and Stage 3 produce SHA-256-identical outputs. The fixed point is the proof of correctness.
Effects live in the signature
The checker reads colour before you read the name.
Nine algebraic effects, plus linear as a type qualifier. A solid border is written in
with. A dashed border is recovered from a callee. A struck badge is no longer
live in this frame. A function without with IO cannot call one that has it.
fn read_sensor () -> Knowledge<f64> with IO Observe
website/src/pages/language.astro · effectsExample · subset rule, not a handler
fn calibrate (sensor: &!Sensor, bias: f64) with Mut
with &! is exclusive mutation, not Rust &mut. The three
renderings are the badge vocabulary. This page does not claim Sounio has effect handlers.
Tokens: --color-effect-{io,mut,div,panic,alloc,async,gpu,prob,observe} and
--color-type-linear. Linear is a type qualifier, not a tenth effect.
Three-stage bootstrap.
No trust in the seed binary is required. Reproducibility is the guarantee: if gen2.elf and gen3.elf differ, the compiler has a bug.
Stage 0
C-compiled seed
A minimal C implementation of the Sounio parser and emitter. Its sole job is to compile lean_single.sio into a working binary. Not trusted beyond Stage 1.
Stage 1
First self-hosted
The seed binary compiles lean_single.sio into gen1.elf. This is the first Sounio binary compiled by Sounio.
Stage 2 ≡ Stage 3
Fixed-point verified
gen1.elf → gen2.elf, then gen2.elf → gen3.elf. The SHA-256 of both must be identical. This is the compiler's self-consistency proof.
Run it yourself
# Stage 0 → 1: C seed compiles the Sounio compiler
./artifacts/self-hosted/souc-self-hosted-x86_64 \
self-hosted/compiler/lean_single.sio gen1.elf
# Stage 1 → 2: first self-hosted compile
./gen1.elf self-hosted/compiler/lean_single.sio gen2.elf
# Stage 2 → 3: fixed-point check
./gen2.elf self-hosted/compiler/lean_single.sio gen3.elf
# These two SHA-256 digests must be identical.
sha256sum gen2.elf gen3.elfFour compiler phases.
Each phase is a separate module in self-hosted/compiler/. Epistemic types are tracked through every phase; the confidence lattice is never erased between HLIR and emit.
Parse
parser/items.sio
Recursive-descent parser. Produces an unresolved AST including effect annotations, where clauses, and algebra declarations. No implicit token recovery — ill-formed input is a hard error.
Check
check/mod.sio
Type checker with bidirectional inference. Resolves Knowledge<T> widening, effect-row unification, and confidence gate constraints. All epistemic obligations are discharged here or rejected with a typed error.
HLIR
hlir/mod.sio
High-level intermediate representation. E-graph rewriting with 1000+ rules runs here. GUM uncertainty propagation is lowered into explicit variance-carrying nodes before emit.
Emit
emit/mod.sio
Backend dispatcher. The shipped path is x86_64 native (System V ABI, static Linux ELF). The GPU path emits PTX for a skeleton of named kernel patterns only (TOUR.md §6). Linear types enforce that every resource is consumed exactly once.
One shipped target.
The compiler targets Linux x86-64 only (TOUR.md §6). The epistemic layer is not a runtime library — it is lowered into the same machine code that carries the computation. Other emitters in the source tree are drafts or skeletons, listed here so their status is not overread.
x86_64
Shipped
System V ABI. The primary development and production target. souc itself runs here. Knowledge<T> confidence is laid out as a struct field; GUM propagation compiles to scalar arithmetic.
ARM64, macOS, WASM
Not shipped
Not supported targets. The binaries are static Linux ELF and do not run on macOS. The WASM backend is a blocked draft (#2237). The Cranelift JIT is no longer shipped (CHANGELOG 2.1.0).
PTX
Emission skeleton
souc build --backend gpu emits valid PTX for a skeleton of named kernel patterns: kernels with empty bodies, no arithmetic and no memory access (measured 2026-10-04, examples/kernel_vec_add.sio). It is not a general GPU backend.
Lean 4 for the hard proofs.
Where the type checker enforces, Lean verifies. The two key properties of the epistemic type system — GUM conservativity and confidence monotonicity — are stated as theorems and proved in formal/EpistemicEffects.lean.
gum_conservativity
Proved
GUM uncertainty propagation through arithmetic never increases confidence. A composition of epistemic operations cannot manufacture certainty that wasn't present in the inputs.
confidence_monotonicity
Proved
Widening a Knowledge<T> value (increasing ε) cannot produce a narrower confidence interval. The ordering on the confidence lattice is monotone through all type operations.
substitution_lemma
Open obligation
Substitution of epistemic values in effect-typed terms preserves the effect row. Proof structure is in place; one indexed-induction obligation remains.
Source:
formal/lean4/EpistemicEffects.lean
(589 lines, 0 sorry).