The Type Checker Passed and the Formatter Said Nothing

Now that a model can produce hundreds of lines of syntactically valid code on demand, the rate limit on productivity is no longer how fast you write but how fast you review and verify. I think that diagnosis is right. And the prescription is usually written in language features: static types reject hallucinations, a formatter erases stylistic drift, fast compilation drives a self-correction loop, a thick standard library keeps dubious dependencies out. The last line of defence is code a human can read quickly.

I spent last week moving a compiler from v0.1.263 to v0.1.273 — Mere, a language of my own with five backends (interpreter, C, LLVM, Wasm, RV32I). I was migrating the string representation, making failure mean the same thing everywhere, and fixing tail calls. If the diagnosis is right, a week of that ought to say something about how well the prescription works. When I counted, not one of the things that caught an error was inside the language.

What follows is not an advertisement for Mere. A system with five implementations happens to be good at producing this kind of record, and that is the only reason it is the evidence here.

One week, tabulated

What was going on	Static types	Formatter	A human reading	What actually caught it
A self-hosted backend kept the old string representation and stamped the same ABI number	passed	silent	went unnoticed for three days	a differential test making four implementations print the same value
nan < 0.0 was true on the interpreter only	passed	silent	invisible	a new gate written with values that had just become writable
“key is missing” was uncatchable on three compiled backends	passed	silent	invisible	a value-range gate over collections
str_repeat s 0 allocated without a length field, on LLVM only	passed	silent	invisible	a value-range gate over strings
list_filter alone was not tail-recursive	passed	silent	invisible	a gate at 100,000 elements, then grep
Stack overflow had no name; two backends died silently	out of scope	out of scope	no cause of death	a set of programs expected to fail
A gate was testing a three-day-old binary	—	—	misread as “the code is broken”	suspecting the gap between CI and my machine
A pin that was no longer true stayed on disk	out of scope	out of scope	nobody notices	making the expiry of a pin itself a failure

The third column caught nothing. Since that column is where the prescription puts its last line of defence, this is not a small thing.

Guardrails protect one program; gates protect the question

The reason is that they guard different objects. A type checker and a formatter both look at the internal consistency of the one program in front of them. Is the representation coherent, do the names resolve, is the layout uniform. Each of those is the question “does this program contradict itself?”

Every row above was healthy under that question. The code stamping the ABI number type-checks. The nan comparison type-checks. The shell script testing a three-day-old binary was, in itself, working correctly. The contradiction was not inside one program. It was between two things — between two implementations, between a declaration and an implementation, between the thing doing the checking and the thing being checked.

A tool that looks inside one program cannot reach there.

Three of them, in more detail.

An ABI number is a claim, not a check. This system promises a representation across the boundary between a Wasm module and a JS host, and names that promise with an ABI number. A string is “four bytes of length, then the body, then a NUL”, and the value points at the start of the body. But there are two compilers that produce modules: the OCaml implementation, and the one compiled by the language itself. The self-hosted one still had the older representation, with no length field, and it was stamping the same number. A host that believed the length field printed 567KB of NUL for a single string. Numbers matching does not mean implementations match. If two or more implementations claim the same number, you need a check that compares behaviour rather than numbers. What caught it was a test that makes four implementations print the same string.

A gate must not cache the thing it is testing. The self-host check failed all seven of its cases. The compiler was not broken. The script builds the self-hosted compiler into /tmp, and it was written as “build it if the file is absent.” What was there was three days old, from before the ABI change, and the gate was testing a compiler nobody had asked about. Caching inputs, oracles, and vendored data is correct. Cache the subject and the gate tests something else.

That lie has an awkward shape: it arrives wearing the face of a real defect. Not a silent green but a red, so the obvious inference — the gate is red, therefore the code is bad — runs unopposed. And CI never disagreed. The runner starts with an empty /tmp, so it built the thing fresh every time and was always green. The same commit was green on a machine nobody was watching and red on the machine I was working on, and the red one was the wrong answer. Building it every time takes 260 milliseconds. There was never a reason to cache it.

Make the gate detect “no longer violated” too. This system has a way to keep a difference it cannot fix without deleting the test: when one implementation answers differently, the difference is written down as a declaration and held there. But once such a difference started agreeing, the test passed in silence — an agreeing case never reads the declaration. So a declaration that was no longer true stayed on disk, which is exactly what the mechanism exists to prevent. After expired declarations were made failures, the thing that told me that week’s work was finished was that new failure. Detecting violations alone does not let a fix erase its own record.

About the “a human reading” column

This is not an argument that readability is worthless. None of those fixes would have been possible in a language you cannot read. But the picture of the workflow — the AI writes, the human verifies — did not match what the week actually looked like. What happened was that the machine verified, and the human’s job was designing the question to ask.

That explains why every rule I came away with that week was about the design of the question. A gate must not cache its subject. A gate says how many cases it checked (zero is indistinguishable from “did not run”). An oracle has a version, so pin it and print what you compared against. Do not reach agreement by declining to ask. Carry two numbers, because one can move when the other does not. Separate a skip for a missing dependency from a skip for a real failure. Not one of those is about readability.

What about proofs?

The guardrails so far have meant the type checker and the formatter. That is not the strongest form of the argument. MoonBit made formal verification a first-class part of the language in 0.9 — contracts, predicates, loop invariants and proof_assert are syntax, and the compiler understands them directly. The stated aim is explicitly for AI: code that is not merely functional but provably correct. That reaches much further than a type checker, and the dichotomy above does not account for it.

Accounting for it, I think the conclusion holds, because a proof and a gate fail differently.

A proof answers “does the implementation satisfy the specification,” and the specification is something a human wrote. Read the rows above again and every one of them is a case where nobody had written down the claim that was violated.

• The ABI number was a specification. It says a string is “four bytes of length, then the body, then a NUL.” What was broken was not the relation between an implementation and that spec — it was that two implementations claimed the same spec and one of them was a different thing. Neither implementation lies about itself.
• A gate testing a three-day-old binary is not saved by having a correct specification of the thing it tests, because the wrong compiler satisfied the spec. The question was not “did the check run correctly” but “what was checked.”
• An expired pin was a specification that was no longer true. A mechanism that holds implementations against specifications does not tell you a specification has gone stale.

Gates have their own way of breaking, which is the next section.

Neither subsumes the other. A proof is bounded by the quality of the specification; a gate is bounded by the independence of the things it compares. And there is a range only the proof reaches: for bugs expressible as a contract — bounds, invariants — formal verification is strictly stronger than what I have, because it answers for all inputs rather than the ones a gate happened to ask about. str_repeat s 0 in the table is on that side. A contract saying the result always carries a valid length would have caught it without anyone thinking to try zero.

Which narrows the claim usefully. Not “the answer is outside the language” but: for this week, everything that worked was outside the language — and the language-side mechanism that could have reached some of it is proof, not types.

Two limits

The claim has limits, and I walked into one of them the same week.

Agreement is evidence only when the things agreeing are independent. Not long before, I fixed a function that reads 32 bits big-endian out of memory and was sign-extending them. An opaque pixel has alpha 0xFF, so every program that touches pixels hits this. But the differential test across five implementations did not catch it, because the JS host had exactly the same bug (it was using getInt32). Comparing implementations reaches further than a type checker, but it is not invincible. It works only as far as independence holds. Writing “differential tests will protect you” without saying that would be the same species of overstatement as “the type checker will protect you.”

And this is one person, one project, one week. The eight rows are specific and dated, but eight rows are eight rows. You cannot get “language features do not help verification” out of this. What you can get is much narrower: for at least this one week, everything that worked was outside the language — one counterexample, and no more than that.

If there is an implication for language design

I do not think it is “add more guardrails.” It is be shaped so that gates can be placed. Concretely, three things.

First, more than one place that can answer the same question independently. Most of the defects this system found that week came out of asking five implementations the same thing. A single-implementation language cannot have that check at all. Normative corpora and diffs against someone else’s implementation are substitutes, but they are substitutes you have to arrange from outside the language.

Second, being able to ask the compiler what exists. This system used to keep hand-written tables of which backend had which builtin, and all three of the tables had gone stale. A table you cannot trust is worse than no table. Now the table is generated by querying the compiler and diffed on every run. Against the problem of a model reading stale documentation and writing something false, there is an answer other than auto-updating the documentation: make the documentation an artifact of the build.

Third, a uniform surface for failure. When the same failure has a different name on each backend, a check reports that difference as a real one. That week I found the shape where the most common failure has the least naming. The most frequent way a program in this system actually dies is stack overflow — and that was the one failure the language said nothing about, with two backends silently returning exit code 139. Name the rare failures first (division by zero, a missing key) and the most frequent one is what gets left over as an event from outside the language.

None of the three is about making generated code easier to read. They are about letting a machine keep holding the question. If the diagnosis that verification is the bottleneck is right, that is where the investment goes.