Owner’s question 3 of #796,
2026-10-24: before deciding, what a formal semantics is, where the work sits and
what it would look like. Companion to formal-verification.md
(item 10 of its table). Nothing concrete needs it now: no program, user or
measurement waits on it. It is the precondition of claim (a), a compiler proved
to preserve meaning, which is not aimed at.
A program’s meaning is what it does when it runs: the values it computes, what it prints, where it stops. Today that meaning is written down in two places: in the specification’s prose (Parts I-III, about 6,700 lines), and in what the compiler does, because a program is lowered to Rust and Rust decides the rest. A formal semantics writes the meaning a third time, as rules in a mathematical notation, so precise that a machine can check a proof about it. It is to the prose what a grammar is to “a statement is roughly a line”.
Take this program (probed on target/fast/nikaia, 0.0.1204):
enum Shape {
Square(i64),
Rect { w: i64, h: i64 },
}
fn area(s: Shape) -> i64 sync {
return match s {
Shape::Square(a) => a * a,
Shape::Rect { w, h } => w * h,
}
}
fn sum_to(n: i64) -> i64 sync {
let mut s = 0
let mut i = 1
while i <= n {
s += i
i += 1
}
return s
}area(Shape::Rect { w: 3, h: 4 }) prints 12, sum_to(10) prints 55, and
area(Shape::Square(4000000000)) stops the program: the text is Rust’s
attempt to multiply with overflow, from the lowered ex.rs. nikaia check
--bounds keeps all four arithmetic checks (a product of two unknowns, #386;
no fact bounds what it reads, #432). nikaia interpret prints {} {}: the
interpreter (tools/interpreter.nika, 129 lines) walks main and evaluates
nothing (Stage 0). So no part of the toolchain today computes a program’s
meaning except the compiled binary.
Prose (Part I, as written today):
while loop repeats its body as long as its condition is true.match expression compares a value against a series of patterns;
else is the arm taken when nothing above matched.Formal, big-step (one common notation; σ is the store, the values of the
names; ⇓ reads evaluates to; above the line what must hold, below it what
follows):
⟨e₁,σ⟩ ⇓ n₁ ⟨e₂,σ⟩ ⇓ n₂ n₁·n₂ ∈ [−2⁶³, 2⁶³−1] ⟨e₁,σ⟩ ⇓ n₁ ⟨e₂,σ⟩ ⇓ n₂ n₁·n₂ ∉ [−2⁶³, 2⁶³−1]
───────────────────────────────────────────── MUL ───────────────────────────────────────────── MUL-STOP
⟨e₁ * e₂, σ⟩ ⇓ n₁·n₂ ⟨e₁ * e₂, σ⟩ ⇓ stop(overflow)
⟨c,σ⟩ ⇓ false ⟨c,σ⟩ ⇓ true ⟨b,σ⟩ ⇓ σ′ ⟨while c b, σ′⟩ ⇓ σ″
─────────────────────── WHILE-END ──────────────────────────────────────────────── WHILE-TURN
⟨while c b, σ⟩ ⇓ σ ⟨while c b, σ⟩ ⇓ σ″
⟨e,σ⟩ ⇓ v armᵢ = pᵢ => eᵢ ∀j<i: match(pⱼ,v) = no match(pᵢ,v) = θ ⟨eᵢ, σ ∪ θ⟩ ⇓ r
───────────────────────────────────────────────────────────────────────────────── MATCH
⟨match e { arm₁ … armₖ }, σ⟩ ⇓ rplus one rule per pattern shape for match(p,v) (seven plus eight in 3.4), a
rule for stop passing outward through every construct (an e₁ that stops
stops the product), and the typing rules beside them: for example a match
over an enum is complete when every variant is named, the static side of
NK1151, which is what makes the ∀j<i … no never run off the end.
What writing them found at once (checked in Parts I-II, 2026-10-24):
f() * g() runs f or g first. MUL above silently chose left to
right. With a print in each function the two choices are two different
programs; today Rust’s left-to-right decides.stop? 2.2 says the program stops; A.2 of Part III gives the
exit status; the text a user sees is Rust’s panic message. A formal rule must
say whether the message is part of the meaning.async
pauses and overlap need small-step rules (one step at a time) or a
coinductive reading. That is a choice of style with real cost.match reads what it binds (3.4, 6.5): whether an arm takes a view or
moves the value changes what s is afterwards. σ ∪ θ above hides that; the
real rule needs a store that knows owned, viewed and moved places.| Part of the language | Difficulty | Why |
|---|---|---|
Integers, overflow, wrapping_/checked_, if, loops, match, structs, enums, calls |
low | textbook; the rules above; floats need IEEE-754 as a library |
T?, ??, throws/try, panic, break/continue/return |
low-medium | one outcome kind each, passed outward |
Ownership, ref, views, the four doors (Ch. 6), the tether and the ledger |
high | RustBelt and Stacked/Tree Borrows show the size: research-level; the typing side (what is refused) is larger than the running side |
async by default, overlap, spawn, user_parallelism (Ch. 8) |
high | needs small-step, interleavings and a memory model for shared data |
comptime, build-time code (Part II) |
medium | the same rules run at build time; the hard part is what the build may observe |
| Traits, generics, monomorphisation | medium | elaboration into a core first, then the core’s rules |
Text (bytes, scalars, graphemes), collections, std |
medium, large | each std entry is a rule or a model; Unicode tables as data |
Effects, input/output, extern "C", unsafe, assume |
outside | modelled as an oracle; unsafe is where the semantics stops promising |
Rough size, from comparable work and from memory, not measured: a core (first two rows, no ownership, no concurrency) is a few hundred rules, some thousands of lines in a proof assistant; the whole of Part I with ownership and concurrency is comparable to the Wasm or CompCert C semantics, tens of thousands of lines and person-years.
Tools. Proofs need a proof assistant: Lean 4, Rocq (Coq) or Isabelle (Wasm
has all three; CompCert Rocq; CakeML HOL4); the K framework gives executable
semantics with less proof power. A Nikaia-hosted model (the rules written as
a definitional interpreter in tools/*.nika) honours CLAUDE.md’s rule that our
own tools are written in Nikaia and serves uses 1 and 4, but it cannot prove:
Nikaia’s prover is linear arithmetic, not a logic for theorems about
programs. A proof in Lean is not a helper tool but it is code in another
language; that would be an exception to the rule, and it is the owner’s.
| Level | What | Serves | Cost |
|---|---|---|---|
| 0 | Prose as today | - | - |
| 1 | Paper rules for a core, beside the prose (as the Wasm specification does), not machine-checked | gaps (1) | small; drifts unless kept with the prose |
| 2 | Executable semantics: a reference interpreter in Nikaia, one function per rule, each citing its section; the compiled binary diffed against it on the suite and on generated programs | gaps (1), oracle (4), a second implementation (5) | medium; replaces today’s Stage 0 interpreter, so it is a new build, not a check of an existing one |
| 3 | Mechanised core in a proof assistant; type soundness of the core | (2), (3) for the core | large; another language |
| 4 | CompCert-style preservation of the lowering | (2) in full | person-years (item 14) |
Not levels 3-4 now. Level 1 for the core of Part I, written into the
specification as rules, is cheap and would already have found operand order;
level 2 is optional and no step towards claim (b), which needs no interpreter
(formal-verification.md 7); it is worth it once self-hosting has moved check and emit (#125 C-7
and E10/E11), as the oracle for a lowering that then no longer has a Rust twin
to be compared with. Not decided here: whether Part I takes formal rules at all
(STYLE.md would need a notation), and whether a proof assistant may ever enter
the repository.