Cheng Tan

The Old Bargain

Formal methods deliver certainty, but in a language few engineers write or read

· systemsresearchai ·中文

In 2009, NICTA finished a proof of the seL4 operating-system kernel. The kernel is 8,700 lines of C and 600 lines of assembler; its Isabelle proof is 200,000 lines. Building the kernel took about 2.2 person-years. Proving it took about twenty. Two years earlier, CompCert had done the same for a C compiler: 42,000 lines of Coq, now the Rocq Prover, of which 76% is the proof that compilation preserves what your program means. IronFleet later verified two distributed systems and reported a detail that deserves to be better known: both worked the first time they were run.

That is not a story of failure. It is a story of complete success inside a boundary that has never moved. Almost all software is written outside it. Cost explains part of that, and the rest is easier to see by looking at what Hoare logic actually does.

What the rules do, and what they quietly don’t

Hoare logic uses a triple: a precondition, a program, a postcondition. Its rules describe how programs compose: sequencing, assignment, iteration. They are small and they are elegant. Then there is the rule of consequence: if a program establishes R, and R implies S, then it establishes S.

Look at the second premise. That implication is not a fact about the program. It is a fact about the assertion language, and Hoare logic does not prove it. It assumes someone else can. The program rules supply structure; the mathematical content sits in the side conditions.

Cook made this precise in 1978. Hoare logic cannot be complete outright, for reasons that go back to Tarski rather than to engineering, but it is complete relative to an oracle: complete if, mid-proof, you may consult the set of true assertions and be told the answer. The standard history of the subject describes the move as using the true assertions as an oracle “that can be freely consulted in the correctness proof.”

So predicate logic is the subroutine and Hoare logic is the calling convention, and everything hard about verifying a program is hard in the assertion language rather than in the program logic wrapped around it. Fifty years of tooling has been, in effect, fifty years of building better oracles: decision procedures, SMT solvers, tactic languages, proof automation. The calling convention never changed.

Two bills, and the second one is worse

The visible bill is proof effort, and everyone quotes it. Twenty person-years against two. Seventy-six percent of the file. IronFleet worked hard to get its implementation-layer ratio down to 3.6 lines of proof annotation per line of executable code, which was a real achievement and is still 3.6.

The quieter bill is the specification, and it resists itemizing. Before any of this begins, someone must write down what the system is supposed to do, in logic, and nothing checks that statement. It is the axiom at the top. IronFleet’s authors are direct about it: the trusted specification for IronRSL is 85 lines and for IronKV is 34, “making them easy to inspect for correctness.” Easy to inspect, by a person, reading it.

At the top of every verified system in the world there is a paragraph someone read and believed.

seL4 draws the rest of its perimeter carefully: “We assume the correctness of the compiler, assembly code, boot code, management of caches, and the hardware; we prove everything else.” That is a clean line, drawn in public. But the same paper contains a quieter sentence, about the kernel’s own virtual-memory window: “We make this consistency argument only informally; our model does not oblige us to prove it.” Even at the high-water mark of machine-checked systems software, there is a seam where the proof stops and a competent person says and clearly.

Verifications are not messages

In 1979, De Millo, Lipton, and Perlis predicted that program verification was bound to fail. They were wrong, and it is worth saying so first: seL4 exists, CompCert ships inside avionics toolchains, and thirty years of work by people who read their paper refutes the forecast.

What survives is the observation underneath. Mathematical proofs earn confidence socially: they get read, restated, taught, doubted, patched, and eventually absorbed. Program verifications cannot enter that process, because of what they are:

Verifications are not messages; a person who ran out into the hall to communicate his latest verification would rapidly find himself a social pariah.

Their blunter version: “Verifications are long and involved but shallow; that’s what’s wrong with them.” A 200,000-line Isabelle script is a valuable certificate. You can check it, and checking it is worth a great deal. You cannot read it, disagree with one part of it, quote it in a design review, or use it to show a new engineer why the kernel is safe. The knowledge exists and does not circulate.

They saw the specification problem too, in a sentence that has not needed revision in forty-five years: “The specifications for any reasonable compiler or operating system fill volumes—and no one believes that they are complete.”

The terms

Translate your intent into a formal assertion language, and a machine will check everything downstream of that translation, with certainty.

It is a good bargain, and the evidence for it is overwhelming. But notice what you pay, because neither charge falls with scale. You must be able to make the translation at all, which rules out every property you can state in English and not in logic, and there are many. And what comes back is a certificate rather than an argument a colleague can follow.

That is why verification concentrates where the stakes pay for it: kernels, compilers, cryptography, flight control. Everywhere else, correctness arguments still get made in English, constantly, and nothing checks them.

The next question is not how to make formal proofs cheaper. It is what happens when the assertion language changes.

References