What the Checker Actually Proves

The report separates “proved” from “admitted by assumption” on purpose: a checker that silently accepts what it has not checked is worse than none. Header of the checker’s main module (translation)

Every answer in this book came with a proof attached. The proof is a graph: leaves that point at facts, steps that name a rule and the values substituted into it, a root that states the answer. I have shown you those graphs as tables and told you what they contain. I have not yet told you who reads them.

Here is the question the chapter turns on. Suppose someone hands you a proof graph and says the machine produced it. What would it take for you to believe it, without trusting the machine?

Most people’s first answer is “run the machine again and compare”. An independent implementation makes that comparison stronger, but agreement is not proof: two readings can share a mistaken premise or the same omission. This is a principle of the method, even when every comparison agrees. The second answer is the subject of the rest of the chapter. You believe the proof if something that is not the machine, and knows nothing about how the machine works, checks every step against the rules and accepts.

That something exists. It is a third program, written in a language built for proofs, and the interesting thing about it is not that it accepts. It is how carefully it says what it did not check.

The second witness

Two separately written programs can be asked the same question under the same rules. Compare each answer with the other and with an expected answer written from the rules before either program runs. A disagreement then points to a question that needs investigation: did one program misapply a rule, did the expected answer misread it, or was the rule itself ambiguous?

Independence matters. Making one program copy the other removes the second witness. The expectation needs its own grounds too: it should come from the source and the chosen reading, rather than from whichever answer happens to be convenient.

Consider the remainder when minus seven is divided by three. Under a Euclidean convention it is two; a convention that truncates the quotient toward zero gives minus one. A comparison becomes meaningful only after the intended convention has been stated. Agreement checks the application of that convention, not the wisdom of choosing it.

Agreement means two independent readings of the same text landed in the same place. That is useful evidence, and it is not proof. Shared premises remain shared premises however many programs repeat them. For proof there is a third witness.

The third witness

The checker is small. Small enough to read in an afternoon, and written in a language made for checking proofs rather than for running programs. It imports nothing outside itself: no mathematics library, not even the proof assistant’s own standard tools for reading data, because pulling those in would make the trusted base as large as the tool. The specification asks for a small deterministic checker, and this one is.

It does not run the law. It reads three things: the rules, the case, and the answer with its proof graph. Then, for each node in the graph, it asks one narrow question. For a leaf: does it point at a fact that is really in the case or in the rules, word for word? For a step: does the named rule exist, and does the step’s conclusion follow from its premises by exactly that rule? For the whole graph: does every reference land on a node that exists, and does nothing rest on itself?

Those questions are answered by a function, and the formal core comes with a theorem checked by the proof assistant. Under its CertOK condition, conclusions follow from the formal rules and supplied base facts. The operational checker can also accept steps by explicit admission: those steps remain assumptions, and accepting a certificate does not discharge them. The theorem’s proof has no sorry gaps; this does not mean that every accepted certificate is assumption-free. The experimental notes record the theorem’s premises and its logical dependencies.

Read that carefully, because it is easy to hear more than it says. The theorem does not say the answer is right. For the steps it verifies, it checks inference against the specification’s definition of “follows”; admitted steps retain their assumptions. If the rules are a bad model of the statute, the certificate is a valid proof of a bad model. If a fact was accepted that should not have been, the proof stands on it. The checker certifies inference, and only inference.

What it says it did not check

Every line of the checker’s report says one of two things about a node. The checker checked this step. Or the checker admitted this step without checking it, and here is why. The commonest reason is that the step is of a kind the checker cannot check yet. That is a reason for admitting, not a third kind of result, and the reader should hold on to the distinction: an admitted step is not wrong, it is unexamined.

I ran the checker on two certificates on the day of this chapter, in its verbose mode, where it prints every admission it was forced to make.

The first was the simplest case in the collection: a fact asserted, and the question whether it is established. Two nodes. One leaf checked, one query checked, no admissions. The checker said it had verified the certificate by its proven function, and it had.

The second was a remainder case, minus seven modulo three. Three nodes. One leaf checked. Then a line I want you to see: the rule step is admitted, not checked, because its conclusion contains an arithmetic term, and the checker’s current version does not do that arithmetic. And a second line: the query’s “established” rests on an unchecked step. The checker still said OK, but the OK now carries two named admissions. Successful validation is not necessarily an assumption-free proof: readers must inspect both the verified steps and the admissions.

On the evidence case of chapter three the report is longer, and one line in it deserves a plain translation. For each document that became a fact, the checker says that it confirmed which document the fact refers to, and that whether the fact was rightly read out of the document is not something it checks. The reading of documents is outside the core, and the checker says so eight times, once per document.

That is the design, and the sentence at the head of this chapter is its reason. A checker that prints “OK” and nothing else is a checker whose OK cannot be read. This one prints “checked” and “admitted” in separate columns, and on real acts the second column is not small: about a third of the rule steps in the corpus’s certificates are admitted rather than checked. Most of those are rules marked as defeasible. Applying such a rule produces a candidate, not a conclusion; the candidate may still be defeated. The checker reads the rule’s strength and refuses to count the step as checked. The distinction matters: a formula for a health-insurance contribution can be arithmetically right while the obligation it computes remains presumptive, subject to an exemption the arithmetic does not establish.

Forging a certificate

A checker that never says no is decoration. So the method includes a set of forged certificates, a premise removed, a fact altered, a conclusion swapped, a reference into nowhere, and the check that runs the checker over the whole corpus also runs the forgeries and requires each to be rejected.

I made one of my own by hand, on a certificate from the corpus with a genuine rule step in it, to see a refusal rather than read about it. The certificate has four nodes: a fact, a rule step, a query, and one node outside the core. Genuine, it passes. I deleted one premise from the step and ran the checker again. Refused: the step’s conclusion no longer follows from what is left.

The refusal is the product. A proof graph that a third program will reject when one premise is deleted is a proof graph you can hand to an opponent.

A graph must contain its grounds

Take a document that computes a total. Its root cites intermediate steps as premises. If those steps are absent, the certificate has not supplied the grounds it asks us to accept. Two programs could emit that same incomplete graph and agree exactly. The comparison would establish their agreement; it would not supply the missing steps.

A checker asks a different question. Every premise reference must lead to a node in the certificate, and the chain must not rest on itself. Closure and freedom from cycles are separate requirements: a graph can have no cycle and still point into nowhere. Both must be checked.

Likewise, a list of supporting facts must have the form the certificate contract requires. If that contract treats the list as a set, duplicates or a noncanonical order are grounds for refusal. A refusal tells us which requirement was not met; agreement between producers cannot override it.

What it does not know

The boundaries, since the checker names them itself and I would be misrepresenting it to leave them out.

It does not do division, or sums over collections. It does do multiplication, rounding and comparison of exact decimals, with arithmetic of its own, so that a computed contribution is recomputed rather than trusted.

It does not prove that a defeasible conclusion survives. It recomputes the set of defeats and compares it with the document, rejecting a missing defeat and an extra one alike, but a surviving candidate is still a candidate. Conditional priorities between rules it does not attempt.

The checker validates individual derivations but does not independently establish that the engine has found every derivable conclusion. Certifying the absence of support would require an additional completeness argument. “Refuted” reports support for the opposite proposition; checking that support is different from proving that no positive support was missed.

It does not prove completeness. That every derivable fact has a certificate is a property of the engine; the checker’s job is to be strict, not to be generous.

And it does not read the statute. Nothing in the third witness knows what a turnip is, or a tenge, or a good-faith purchaser. It knows rules, substitutions and what follows from them, and it tells you, one line per node, where its knowledge stopped.

The proof is not the truth

This is the sentence Part Three is named for, and the checker is where it stops being a slogan.

A certificate that passes the checker establishes exactly this: for every step the checker checked, the conclusion follows from these rules and these facts by the specification’s definition of following; and for the steps it admitted, it has told you it admitted them, and why. That is a great deal more than “the machine says so”. It is a great deal less than “this is the law”.

Between the two lies everything the earlier chapters were about: whether the rules are the statute, whether the facts were admitted rightly, which reading was chosen, what the model leaves out, what the court will decide. The checker cannot see any of it, and its honesty consists in never pretending to. When you hold a certificate that passed, you hold a proof of the steps it checked and a list of the steps it took on trust. Whether you hold the truth is the question the proof was never asked.