DEV Community: arcker

A compiler written in its own language just emitted a standalone Linux executable

arcker — Sun, 21 Jun 2026 08:47:45 +0000

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.

Every elevator has a load plate. Tests are supposed to kill fear, not feed it.

arcker — Sun, 14 Jun 2026 14:37:31 +0000

Every elevator has a small metal plate near the doors: 8 persons — 630 kg. It doesn't mean the car snaps at the ninth person. It means an engineer loaded it, measured it, and signed an envelope: this is what I guarantee, within these limits, with margin. The plate isn't a confession of weakness. It's the exact thing that lets you step in without a second thought.

I build Lithair — a small, memory-first Rust web framework. This post isn't about its API; it stands on its own. It's about a sentence I've come to believe — DevOps without the test isn't DevOps — and the reason for it is probably not the one you expect. It's not about laziness. It's about fear.

The plate is permission to stop worrying

Look around and the load-bearing things in the physical world all carry their envelope stamped on the outside. A bridge has a weight rating. A cable has an amperage. A climbing carabiner has a kN number etched into the spine. None of those numbers are bureaucracy. Each one is permission: you don't have to be afraid of this, here's exactly how far it's been taken. The plate converts a private unknown into a public, re-checkable fact, and the reward for that conversion is that nobody has to feel the unknown anymore.

That is what a test is for. Not a gate. Not a ritual. A way to stop being afraid of your own system.

What I've actually seen

I've spent years around enterprise software, and when real testing existed, it usually wore one of two shapes — and both, underneath, were shaped by fear.

There were the dedicated performance teams: a silo you handed the question to, where the schedule was measured in quarters, and where sometimes the software itself had to be bent to fit the benchmark rather than the other way around. Real rigor, but distant — the envelope lived in someone else's backlog.

And there were the functional-test teams who panicked the moment anyone touched anything. Change the color of a logo and you'd get a straight face and the words "non-regression testing." Not because they were unreasonable — because they had no fast, trustworthy way to know whether your one-line change broke something three modules away. So they did the only thing fear leaves you: they said don't touch it.

I want to be careful here, because it's easy to read this as contempt and it isn't. That fear is completely rational when you can't verify. If I couldn't check, I'd guard the gate too. The tragedy isn't the fear. It's that the one thing built to dissolve it — automated tests, ideally backed by a dedicated tool — so often gets turned into another thing to be afraid of.

Tests are the cure for that fear

A test you actually trust does something quietly radical: it gives you back the right to change things. Change the logo color and the suite tells you, in seconds, that the checkout flow still works. Change the storage engine and the harness tells you the throughput still holds. The fear doesn't get managed or scheduled or escalated — it just leaves, because the unknown it fed on is now a number on a screen.

That's the whole point of the plate. You can step into the elevator because someone already took it to the edge and wrote down where the edge is. Automated tooling is how you stamp that plate cheaply enough to do it for everything, not just the one system important enough to rent a perf team. And DevOps — the actual discipline, not the job title — is made for exactly this: turning "don't touch it" into "touch it freely, the tooling will tell you the truth."

So we built the bench

Lithair's cluster had no performance team behind it and no QA gate in front of it. There was just the question — what does it hold? — and nobody to hand it to. So the test became the work: we wrote our own stress harness and ran it until the numbers stopped being opinions.

A three-node cluster. 170,200 writes. Zero drops, zero panics, zero replication divergence across all three nodes. Good numbers — but the one that actually matters isn't a success, it's a ceiling: ~210–240 single-writes per second, per leader. Past that wall, the latency you measure isn't instability — it's pure queueing against the ceiling. The mild decay over a long run (241 → 206 ops/s) traces to in-memory state growth, which is exactly what a memory-first design predicts — not a leak.

We wrote all of it down. That's the plate. And the real payoff isn't the throughput number — it's that I can now change the cluster code and not be afraid of it, because the harness will tell me the moment I leave the envelope.

A plate only kills fear if it's honest

This is the part that's tempting to skip. A load rating that hides its caveats is worse than none, because it manufactures fresh fear later — the kind that shows up at 3 a.m. So the runbook names the ugly bits out loud:

The leader election isn't Raft — it's static, lowest live node ID wins. Always keep a node 0.
There's a brief two-leaders window when an old leader rejoins after a partition. Documented and non-blocking — committed split-brain is prevented elsewhere, by majority-ack on writes — but it's real, so it's on the page.
A couple of endpoints are still stubs in this version. Named, not buried.

None of that is comfortable to publish under your own name. All of it belongs on the plate. A caveat you wrote down is one nobody has to discover in production.

Why the test is the deliverable, not the feature

The cluster code already worked before any of this started — replication, election, failover, all running. What it lacked wasn't capability. It lacked a plate, and you cannot stamp a plate you didn't measure.

"Production-ready" without an envelope test is an adjective: you believe it or you don't, and belief is just fear wearing optimism. With the test it becomes a falsifiable claim anyone can re-run — and a falsifiable claim is the only kind that lets a whole team relax. Strip the test out and what's left isn't speed or risk, it's the fear: the "don't touch it," the non-regression theater over a logo color, the silo nobody wants to disturb. DevOps was supposed to be the discipline that retires all of that. Without the test, you've kept the dashboards and the dread, and quietly thrown away the engineering.

You can put a plate on almost anything

The format generalizes to nearly every load-bearing thing you ship:

an API's requests/sec before tail latency cliffs,
a queue's depth before backpressure kicks in,
a batch job's row count before it OOMs,
a cluster's writes/sec before it's just queueing.

It's always the same shape: here's what I hold, here's why it moves, here's where you leave the tested region. And the reward is always the same too — not bragging rights, but the simple ability for you and the people around you to stop being afraid of your own system. Sometimes the entire tax is one afternoon with a stress harness and the nerve to write down what you actually find.

The full numbers, the cluster runbook, and the v0.13.0 release that earned the plate are in the companion post on arcker.org (in French).

A program is a tree — building a Verbose compiler in Verbose

arcker — Sun, 14 Jun 2026 09:11:25 +0000

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: I'm now writing a Verbose compiler in Verbose itself, and this is the foundation brick — how you represent a program as data so a compiler can work on it.

(English version of an article from my French series, originally on arcker.org.)

After cryptography, we take on something more vertiginous: a Verbose compiler written in Verbose. The language starting to describe itself.

Let's be honest up front — it matters. This is not (yet) verbosec compiling the entirety of its own source. What exists today is a complete front end — tokenizer, parser, analyses, interpreter, type checker — written in Verbose, for a toy subset of the language. The whole thing compiled by verbosec to native machine code. Not an interpreted demo: a ~60 KB ELF binary that reads your program and tells you what's wrong with it. That's examples/vexprparse.verbose: 102 concepts, 219 rules.

We'll walk through it brick by brick. This chapter lays the foundation without which nothing else exists: how to represent a program.

Why write the compiler in Verbose?

The question deserves an answer, because it isn't just an exercise — it touches Verbose's whole thesis.

Today, the compiler (verbosec) is written in Rust. And some of the logic — certain primitives — is Rust that emits x86-64 directly, with no Verbose source. The concrete consequence: to audit a Verbose binary, to really understand what it does, at some point you have to read Rust. And trust that Rust — and whoever, or whatever, wrote it.

That's precisely what Verbose refuses. The whole series rests on four words: you don't trust, you verify. You read the source, declared and proven. If the path from source to binary runs through unverifiable Rust, trust leaks out there.

Writing the front end in Verbose moves that logic into the language itself: the tokenizer, the parser, the analyses become a .verbose file, verified under Verbose's proof regime, then compiled native. The auditor reads Verbose, not Rust. The remaining Rust shrinks to a small, stable, trusted-once base (the verifier). Per-binary trust moves from Rust to the proven source.

And it's the ultimate dogfooding: a compiler is the hardest thing to express. If Verbose can describe its own front end, under its own proof regime, then the language isn't a toy — it holds up on the most demanding task there is.

From text to a tree

A compiler can do nothing with flat text. x + y * 2, to a human, is a string of characters; to a compiler, it's a structure — a tree, where the multiplication nests under the addition (operator precedence):

  The text  "x + y * 2"  is really a tree:

            ( + )
           /     \
         x      ( * )
               /     \
             y         2

Everything starts there. Before evaluating, type-checking, or catching an undefined variable — you first have to turn the text into that tree. That's the AST (Abstract Syntax Tree). And to build it, you need a way to represent a tree as data.

A tree is a recursive sum type

This is where the earlier chapters pay off. A tree is declared in Verbose as a sum type — a type that can take several shapes — some of whose shapes reference themselves:

concept Ast
  variants:
    AstNum  of (value : number)
    AstVar  of (start : number, len : number)
    AstBin  of (op : number, lhs : Ast, rhs : Ast)
    AstNeg  of (inner : Ast)
    AstIf   of (cond : Ast, thn : Ast, els : Ast)
    AstCall of (callee_start : number, callee_len : number, args : ArgList)
    ...

Read AstBin: a binary operation holds an operator, a left subtree Ast, and a right subtree Ast. The type contains itself. That's the recursion of a tree: an addition whose two sides are, themselves, expressions. AstIf holds three (condition, then branch, else branch). AstNum and AstVar are leaves — they hold no other Ast.

Our example then becomes, exactly:

  AstBin( + ,
          AstVar(x),
          AstBin( * , AstVar(y), AstNum(2)) )

The tree drawn above, written as a value. And a.b.c? AstField(AstField(AstVar(a), b), c) — the nesting follows the structure.

No pointers: an index arena

One problem remains. Verbose has no heap and no pointers — one of the reasons its binaries are so small and so verifiable. So how do you build a tree of arbitrary size?

The answer: an arena. All nodes live in a single bounded space, and a node points to its children by their index, not by a pointer.

  concept_group VExpr [max_depth: 4096, max_nodes: 65535]

  arena:  [0]  AstVar(x)
          [1]  AstVar(y)
          [2]  AstNum(2)
          [3]  AstBin( * , lhs=1, rhs=2)    ← references indices 1 and 2
          [4]  AstBin( + , lhs=0, rhs=3)    ← the root

The tree is built bottom-up: leaves first, then the nodes that link them. max_depth: 4096, max_nodes: 65535 aren't decorative — they're the static bounds the verifier needs to prove everything stays finite. No dynamic allocation, no possible overflow, and yet a tree of any shape.

In the same group live the tokens, the environments, and the diagnostics — all variants of VExpr, all linked by index. One arena for the whole front end.

Why this brick first

Because everything else plugs into it. The tokenizer will produce Tokens in this arena. The parser will consume them to build Asts. The analyses will walk the tree to find your mistakes. The interpreter will descend it to compute a result. Without a way to represent the tree — recursive, bounded, verifiable — there's no compiler at all.

And it's the direct payoff of what we built before: the recursion of chapter 1, the termination proofs of chapter 3. An AST is the recursive structure par excellence — and Verbose represents it under the same guarantees as everything else: bounded, pointerless, proven finite.

The program has become data. The next chapter builds it from raw text: the tokenizer.

Originally published on arcker.org, where the full series lives.

TLS 1.3 without a library — a real browser does the handshake against Verbose machine code

arcker — Thu, 11 Jun 2026 13:44:22 +0000

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, with no runtime, no GC, no libc. This post stands on its own; you don't need any prior context. And it describes the wildest thing Verbose has done so far.

(English version of an article from my French series, originally on arcker.org.)

When your browser shows a little padlock next to a URL, it has just held a cryptographic conversation with the server — the TLS handshake. That conversation is usually handled by enormous C libraries: OpenSSL, BoringSSL, hundreds of thousands of lines nobody ever reads in full.

This article is the capstone of the crypto arc of the series. It shows the payoff: a real browser opens an HTTPS page served by a binary whose every cryptographic transform — the key exchange, the identity signature, the bulk encryption, the hash — is machine code emitted by Verbose. Not one line of OpenSSL. And the browser, the most demanding TLS client there is, can't tell the difference: it completes the handshake and renders the page.

We build on SHA-256 (chapter 1 of the arc) — it shows up everywhere in TLS. The details of each brick (AES, Ed25519) get their own chapters; here we pull up and watch the whole thing work.

A handshake, in three ideas

Before any encrypted exchange, the browser and the server have to settle three things. That's all of TLS, one sentence each:

Agree on a secret that no eavesdropper can guess, even after hearing the entire conversation (the key exchange).
Prove identity — the server shows a certificate and signs, so you know you're talking to the right party (the signature).
Talk encrypted — once the shared secret exists, everything else is encrypted with a fast symmetric algorithm (the bulk encryption).

On the wire, it looks like this:

  BROWSER                                 SERVER (Verbose binary)
      │                                          │
      │ ─── ClientHello ───────────────────────► │  "here are my algos + my key"
      │ ◄── ServerHello ─────────────────────── │  "here's mine"
      │            (encrypted from here on)       │
      │ ◄── Certificate + signature ──────────── │  "here's who I am, signed"
      │ ─── Finished ──────────────────────────► │
      │ ◄══ HTML page (AES-GCM encrypted) ══════ │  "Hello from Verbose TLS"
      │                                          │

Each of the three ideas needs a cryptographic ingredient. And that's where Verbose comes in.

The ingredients — and where the boundary runs

Here's the part that matters for Verbose's thesis. All the cryptography is Verbose machine code. The host (in Python) only does plumbing: open the socket, frame the TLS messages, and draw the one random secret (os.urandom).

  ┌──────────────────────────────────────────────────────────┐
  │  HOST (Python)  : socket, TLS record framing,              │
  │                   os.urandom (the only secret input)       │
  ├──────────────────────────────────────────────────────────┤
  │  VERBOSE (x86-64 machine code) :                           │
  │     X25519          the key exchange                       │
  │     Ed25519 / P-256 the identity signature                 │
  │     AES-128-GCM     the bulk encryption                    │
  │     SHA-256 + HKDF  the hash and key derivation             │
  └──────────────────────────────────────────────────────────┘

Every line of the Verbose block was validated byte-for-byte against a reference before being assembled:

AES-128-GCM against the NIST GCM Test Case 2 vector;
X25519 against RFC 7748;
Ed25519 against the three RFC 8032 §7.1 vectors;
HKDF against RFC 5869;
SHA-256, as we saw in chapter 1, against sha256sum.

Nothing is taken on faith because "it worked once." Each brick is checked against the official spec, in isolation, before it's stacked into the next.

The only loop in all of TLS: the X25519 ladder

Almost all the cryptography here is unrolled: each operation finishes in a fixed number of steps the verifier can follow statically. There's exactly one real loop — the X25519 key exchange, which climbs a "ladder" (the Montgomery ladder) over 255 rungs.

In Verbose, a loop is written as recursion, and — like in chapter 3 — it has to prove it terminates:

rule ladder
  logic:
    ...
    out = if s.i == 0 then <the ladder result>
          else ladder(LadderState { ..., i: s.i - 1, ... })
  proofs:
    termination:
      decreasing : i

(The real state carries ~50 fields — the field elements over 10 limbs — elided here.) The key point: decreasing : i is a compile-time-verified promise. The rung i strictly decreases on every call, so the compiler proves the ladder stops. The 255 iterations run at runtime; the guarantee that they finish is established before the binary even exists. No general loop construct was added to do TLS — the proof tools from chapter 3 are enough.

The catch: a real browser doesn't compromise

The first server signed its identity with Ed25519. Against openssl s_client — the usual test client — everything passed: Verify return code: 0 (ok), signature ed25519. We could have declared victory there.

Except a real browser refused. Flat: illegal_parameter.

Why? In its ClientHello, the browser announces the signature schemes it accepts (the signature_algorithms extension). And browsers offer ecdsa_secp256r1_sha256 (P-256), not Ed25519. RFC 8446 requires the server to sign with an offered scheme. Ed25519 wasn't offered → immediate rejection.

That's exactly the value of a real browser as a target: it imposes constraints a test client lets slide. So we had to build the whole ECDSA P-256 stack — GF(p256) field arithmetic, point add/double, scalar multiplication, the modular inverse, and ECDSA-P256-SHA256 signing (RFC 6979 deterministic nonce, DER encoding, low-s) — validated against the RFC 6979 §A.2.5 vectors and openssl dgst -verify.

With a P-256 certificate, the browser stops saying illegal_parameter. It completes the handshake. It renders the page: "Hello from Verbose TLS". The only remaining warning is the expected self-signed-certificate one. Not a crypto failure. The page renders.

The detail that's fun: smaller, for free

Two recursive rewrites, the same week, at zero compute cost:

p256_ninv: 11.2 MB → 84 KB of native code (131× smaller), 8/8 byte-for-byte vs the unrolled version.
x25519_finish: 1.3 MB → 42 KB (31× smaller), 266 field multiplications identical to the unrolled version. openssl handshake re-validated after the cure.

Same algorithm, same exact output, zero CPU overhead. The recursive path introduced for self-hosting (Phase A) turned out to be the right tool for collapsing huge unrolled cryptographic chains into compact machine code.

Why it matters

TLS 1.3 is not a toy: it's a stack of cryptographic primitives, inside a state machine, inside a wire format, with a public client — your browser — that won't compromise on any of it. Making it work end-to-end is empirical proof that the language and its compiler can express, verify, and run a real protocol, not a demo.

And the method is the message. The cryptography here isn't credible because a tool produced it — it's credible because it's confronted, brick by brick, with the RFC vectors, then with OpenSSL, then with a browser that forgives nothing. You don't trust, you verify. That's the whole difference, and that's all of Verbose: a binary small enough to read, proofs declared in source, and output checked against reality at every step.

The arc began with a 12 KB hash in chapter 1. It ends with a browser rendering a page encrypted by a binary you can read line by line. In between, each brick still needs telling in detail — AES, Ed25519, the Montgomery ladder. Those are the next chapters.

Originally published on arcker.org, where the full series lives.