Cheng Tan

Token-Based Logic

Keep Hoare’s structure, change the assertion language, and check small steps

· systemsresearchai ·中文

Hoare logic leaves a deliberate gap. Its rule of consequence asks whether one assertion implies another, and for fifty years the answer has come back from formal logic and a decision procedure. Better solvers, better tactics, better automation, and the gap kept the same shape.

Now imagine filling it with something else. Keep the triples, the invariants, the composition rules. But write the assertions as sentences, and let the judge of whether one sentence follows from another be a reader.

This is no longer a thought experiment. FM-Agent, out of Shanghai Jiao Tong, “generalizes the inference rules of Hoare logic to operate over natural-language specifications,” and it targets no prover at all. The paper is blunt about the consequence: specifications it generates “cannot be used by these tools, as they target formal specifications rather than natural language specifications.” No Lean in the pipeline, no Rocq, no SMT. The oracle is a language model.

That loses certainty. The question is what it buys.

The grain matters more than the language

The bad version of this idea is to hand a model a long argument and ask whether it is correct. Long arguments invite superficial agreement. A reader asked to approve sixty paragraphs will approve them.

So don’t ask that. Cut the argument into steps small enough that each one is a single recognized inference, and check the steps.

Which inferences? There is no closed list, and pretending otherwise would be a mistake, because human reasoning does not come in a finite alphabet. There is deduction, induction, abduction; there is Bayesian updating, causal reasoning, modal and temporal argument, analogy. None of this is a theory of how people think.

The claim is narrower. A few of those patterns have been picked over long enough that we know exactly when they hold, and the categorical syllogism is the most worked-over of them. Two premises, one conclusion, three terms. All A are B; all B are C; therefore all A are C. There are 256 syntactic forms, of which 24 are traditionally valid, or 15 if you decline to assume the categories are non-empty. That last clause is worth a moment: even in the most scrutinized logic anyone ever wrote down, the count of valid forms turns on a semantic convention you have to declare out loud. A system built on natural-language inference will meet that kind of seam constantly, and the seams are where it will break.

In practice the catalogue runs to a dozen entries or so. Barbara sits next to modus ponens and modus tollens, disjunctive syllogism, conjunction and simplification, case split, induction with its hypothesis, and, since the subject is programs, Hoare’s rule of consequence and sequential composition. It claims no completeness. What matters is that every entry has validity conditions fixed in advance, so checking a step means asking whether it instantiates a known shape, not whether it sounds convincing. Granularity is the real design decision: a syllogism-sized step is small enough to judge and large enough to be worth recording.

One move, four costumes

Small steps matter only if they compose, and the composition rule turns out to be something we have been writing down, in different alphabets, for two thousand years.

The same inference appears as Aristotle's Barbara over terms, the chain rule over propositions, Gentzen's cut over sequents, and sequential composition in Hoare logic. In each, a middle element is produced by one premise, consumed by the next, and absent from the conclusion.

In Barbara, the middle term connects subject and predicate and then vanishes from the conclusion. In propositional logic, P implies Q and Q implies R yield P implies R, and Q is gone. In Gentzen’s sequent calculus the move is called cut, and the formula that disappears is named for it. In Hoare logic, a program taking P to Q composes with one taking Q to R, where Q, the intermediate state of the machine, is what the first delivers, what the second requires, and what the composition does not mention.

Four kinds of object: classes, propositions, sequents, program states. One structural move—the cut rule wearing four costumes, as I have taken to calling it. This is the property that lets local checks add up. If every node names its inputs and its output, and each can be judged on its own, then the correctness of the whole argument becomes a property of the graph rather than of anyone’s stamina in reading it end to end. The wiring is ordinary data validation; no model needs to understand a single sentence to check it.

What you are trading

Formal reasoning operates on truth values. Its judge is a decision procedure. It fails by timing out, by meeting an undecidable fragment, or by being handed a formula nobody can write. But when it says yes, it is right.

Token-based reasoning operates on sentences. Its judge is a reader, and it fails by misreading: by being persuaded, by skimming, by agreeing with a fluent step that does not follow. When it says yes, it is probably right, and probably is not something you can prompt away.

Underneath the formal side there is a gradient worth naming. Syllogistic logic is decidable, Boolean satisfiability is NP-complete, first-order predicate logic is semi-decidable, and Hoare logic is undecidable outright—which is why relative completeness is the ceiling. Each level buys expressive power with tractability.

Token-based logic is not the next level on that ladder. It steps off it. There is no complexity class for a competent reader agrees. What it buys is not a larger decidable fragment but the ability to state the premise at all: “the window never contains a repeated character,” “this cache is coherent because a line is never dirty in two places,” “the retry is safe because the operation is idempotent.” Real systems arguments are made of sentences like these, and most of them have no formalization anyone is going to write.

Where the unchecked step lives

Formal verification is not unconditional either, and this part of the comparison usually goes missing.

Its guarantee depends on a translation—from what you meant to what you wrote in logic—and nothing checks that translation. It is the specification: at the top of every verified system is a paragraph someone read and believed. This is not hypothetical. Recent work on autoformalization keeps finding formal and informal statements of the same problem disagreeing, in more than half of the problems in miniF2F, a benchmark of short clean mathematical statements and about as easy as translation ever gets.

So the question is not simply sound versus unsound. It is where you put the unchecked natural-language step. Formal methods put it at the top, once, in the specification, and check everything below it exactly. Token-based methods spread it across every step and check each one approximately.

The first gives a strong guarantee about a statement that may be hard to inspect. The second gives a weak guarantee about statements people can read. Neither dominates. Which you want depends on whether the risk you are losing sleep over is a subtle error below the specification or a mistaken idea above it.

Relative completeness, relative to a reader

Cook’s theorem makes Hoare logic complete relative to an oracle for the true assertions—an oracle that cannot exist, for reasons older than computers, and that we have spent fifty years approximating with solvers.

Token-based logic performs the same substitution with a different oracle: a competent reader. That one cannot be trusted either, but for an entirely different reason. It is not uncomputable; it is wrong sometimes. And unlike the first, you can query it cheaply, about anything you can say, as often as you like.

Which makes the next question empirical rather than philosophical. How often does the reader fail, where, and can you build something that contains the failures? That is what the last chapter is about.

References