A compiler written in its own language just emitted a sta...

Verbose is a small experimental language I'm building. Its compiler proves properties about your code — like termination — and emits tiny, readable x86-64 machine code: no runtime, no GC, no libc. This post stands on its own (you don't need the rest of the series). What it's about: a compiler written in Verbose itself reached the point where a single rule emits a standalone Linux ELF that runs and prints its answer.

Honesty first: this lives on a working branch — not merged, not tagged. It's verified (green test suite, real in-memory execution, a measured benchmark), but it isn't in a released version, and it covers a sub-language (scalar arithmetic), not all of Verbose. More on that at the end.

Two halves of a compiler

A compiler has a half that reads (text → tokens → tree) and a half that writes (tree → machine code). The reading half is the usual story. The new part is the writing half — and the thing that makes it interesting here is that the code generator is itself a Verbose rule. The Rust compiler underneath (verbosec) only runs it; the machine code is emitted by rules written in the language.

Follow factorial all the way down

@proof termination decreasing : n
rule fact (n : number [0, 20]) -> number {
  if n == 0 then 1 else n * fact(n - 1)
}

Note the guardrails that survive all the way to the bytes: @proof termination decreasing : n (the compiler requires proof the recursion ends) and [0, 20] (the declared domain of n). The generator walks this tree and emits, per node:

  n == 0              cmp ; sete            → boolean in a register
  if … then … else …  jz over_then ; <then> ; jmp end ; over_then: <else> ; end:
  n * fact(n - 1)     <compute fact(n-1)> ; imul
  fact(n - 1)         call <offset>         → it calls itself

The jumps carry computed offsets: you only know a jump's distance once both branches are emitted, so the generator runs twice — measure, then write — the way you number a book's pages only after laying it out.

The milestone is that call/ret. When fact calls itself, it's a stack of plates you build up, then unwind while multiplying:

  build up                   unwind (ret)
  fact(3) n=3                3 × 2 = 6   ◄── final
   └ fact(2) n=2             2 × 1 = 2
      └ fact(1) n=1          1 × 1 = 1
         └ fact(0) n=0 ─► 1  (base case)

This is the first time a rule written in Verbose emits machine code that references itself.

From a byte blob to a real executable

Bytes in a buffer don't run on their own — you have to wrap them so Linux will launch them. That wrapper is the ELF format, and the rule now generates the whole thing, like a ready-to-ship parcel:

  ELF64 header         ← "this is a Linux executable"
  LOAD program header  ← "map this into memory, r+x"
  _start               ← call main ; rax → itoa ; sys_write ; sys_exit
  code for main, fact  ← the computation itself

No sections, no symbols, no linked library. A few hundred bytes. The last brick added itoa (int → decimal ASCII) in machine code — without it the binary computed 120 but couldn't show it. Now:

$ ./verbosec examples/factorial.verbose --run lower factorial 5 > a.out
$ chmod +x a.out
$ ./a.out
120

Standalone — no verbosec needed to run the result.

The honest benchmark

The long-standing question — "what does a binary built this way actually buy versus C/Rust/Go?" — finally has a measured answer (Ubuntu 24.04, gcc 13.3, rustc 1.90, go 1.25.4):

  trivial (print a constant, exit)
              size        wall(ms)  RSS(kB)  syscalls
  verbose        512       0.19      352        2
  gcc        706 584       0.24      664       17
  rustc    3 871 984       0.57    2 112       62
  go       2 254 335       1.28    2 132      228

  fib(40) = 102334155  (deep recursion — raw compute)
              size        wall(ms)  RSS(kB)  syscalls
  verbose        635      ~713       352        2
  gcc        706 584      ~135       664       17
  rustc    3 872 832      ~224     2 216       62
  go       2 254 624      ~380     2 232      406

Read it both ways. Wins, by construction: ~1100–1380× smaller than gcc -static, ~6000× vs rustc; two syscalls vs 17–228; RSS down 2–6×. Because there's no runtime — nothing to initialize, no global allocator, no dynamic library. These are audit-defensible: there's almost nothing to audit. Loss, by design: on fib(40), Verbose is ~5× gcc's wall time. The emitted blob has seen no optimizer — no register allocation, no inlining, no constant folding past the AST. That was a decision (a direct, line-by-line auditable emitter, not an LLVM backend), and the compute cost is the price of that legibility — published, not hidden.

What isn't there yet

It's a sub-language: scalar arithmetic (+ − × ÷ %, comparisons, and/or, if/else, let, recursive calls). No strings, no I/O, no services, no TLS.
It's branch-only, not merged, not tagged.
No optimization — deliberately deferred to keep every byte auditable.

The point isn't "Verbose beats gcc." It's "here's exactly what Verbose buys, and what it costs, measured." The read half and the write half of a self-hosting compiler just met one notch closer.

Full walk-through (in French) on arcker.org.

推荐订阅源