Verbose now compiles self-recursive rules to real x86-64 machine code. factorial.verbose produces an 802-byte ELF that computes n! with honest push rbp / call / ret instructions — no interpreter, no inlining. The design document was merged on 2026-05-19. The working binary followed the next day.

What shipped

Four PRs on 2026-05-20, building a composed safety floor:

Phase A slice 5.1a (PR #34) — the call/ret ABI. Self-recursive rules now emit a real callable function at the start of the binary, with the _start loop calling into it via a rel32 backward call. Convention: rdi = input value, rax = return value. emit_eval_expr gained a self_call parameter threaded through 43 call sites. The first binary using this slice was pass-through (statically unreachable recursive arm) — exercises the emit infrastructure without entangling runtime recursion.

Runtime bounds-check (PR #35) — the prerequisite the design review flagged as UNSOUND. A field declared v : number [0, 10] now gets a bounds-check at field-load time (cmp rax, r10 / jl abort). Before: v=1000000 produced one million recursive frames before SIGSEGV. After: exit(1) before the rule body runs. ~38 bytes per bounded field.

Phase A slice 5.1b (PR #36) — first runtime-recursive native binary. The restriction “recursive arg must be Ident(input_name)” is lifted: fact(N { v: n.v - 1 }) now works. Emit: evaluate n.v - 1 via recursive emit_eval_expr, then mov rdi, rax, then call <callable>. Result: factorial.verbose::fact at 802 bytes computes the full factorial table correctly.

Phase A slice 5.2 (PR #37) — text return from recursive callables. Output type text returns via the System-V two-register pair (rax=ptr, rdx=len). The returned pointers point at static data in the binary’s executable region — no stack-allocated buffers that could dangle past ret. Worked example: recursive_label.verbose::label_of at 739 bytes.

Why it matters

Recursive computation is the prerequisite for self-hosting. A verbose tokenizer that scans source text byte-by-byte will recurse. The language can now express that and compile it to machine code, not just interpret it.

The safety composition is the real story. Every slice in Phase A adds one piece, and no piece is accepted until the audit constraint is enforced:

  • Cycle detection (A.5.0) catches infinite loops at compile time
  • Declared bounds (v : number [0, 10]) are enforced at runtime before the first stack frame
  • The compiler emits a mandatory breadcrumb on every recursive binary: “depth bounded by input range, not proven structurally — Phase C will add the proof”

This is what verbose is designed to do: the source expresses the constraint, the compiler verifies it before emitting any code, and the binary fails cleanly when the constraint is violated.

How it works

concept N { v: number [0, 10] }

@intention "compute the factorial of n.v"
@proof "base: v=0 → 1; step: v*fact(v-1), bounded by declared [0,10] range"
rule fact(n: N): number
  out = if n.v == 0 then 1 else n.v * fact(N { v: n.v - 1 })

verbosec factorial.verbose --native fact produces an 802-byte ELF. Run it with echo '{"v":5}' | ./fact and get 120.

The compiler refuses inputs outside [0, 10] before entering the rule — no silent overflow, no unbounded recursion.

What’s next

The current restrictions (single-field input, Number/Bool/Text-literal output, direct self-recursion only) will be lifted in subsequent slices:

  • 5.3: multi-field input concepts at recursive call sites
  • 5.4: mutual recursion
  • 5.5 / 5.6: Result and Record return types
  • Heap-allocated text return (concat + recursion) — needs stack-budget accounting first
  • Phase C: structural termination proofs (replace the mandatory breadcrumb with a verified bound)

Each slice has a named breadcrumb so the deferred bits stay visible.