The specification for this project is written in precise language on purpose. It says things like "this map is a homomorphism" and "these two operations form a lens" rather than "this converts X to Y", because the precise words carry obligations and the vague ones do not.
Nobody had ever checked whether the obligations were met. I built something that reads each claim, resolves the terms against the actual definitions, and returns valid, invalid or unknown.
validity table rows=18 valid=9 invalid=5 unknown=4
Nine of eighteen. Every invalid one was the same mistake in a different costume: a precise word used at the strength of its vague synonym.
One tag byte
The clearest case. The spec said the encoder is a homomorphism into byte strings under concatenation. That is a strong claim with a single obligation:
enc(a · b) = enc(a) ++ enc(b)
Here is what the encoder does for a pair:
enc(pair(x, y)) = tag ++ enc(x) ++ enc(y)
One byte in front, to say what kind of thing follows. That byte is why the encoding is unambiguously decodable, so it is doing real work and it is not going away. It also means the equation is false for every input. Not approximately true, not true up to a constant: there is no pair for which the two sides are equal.
What the encoder actually is, is a map that is injective and prefix-free. Both of those are properties the rest of the system relies on, and neither of them is a homomorphism. The word was reached for because "structure-preserving" felt like the right shape, and nothing ever asked which structure.
Four names for four different things
Another row used DAG, strict order, covering relation and transitive closure as if they named one concept. They are related and they are not interchangeable:
| term | what it is |
|---|---|
| DAG | a graph with no directed cycle |
| strict order | transitive, irreflexive |
| covering relation | the edges of the Hasse diagram, no intermediate element |
| transitive closure | every reachable pair, as an edge |
A DAG is not transitive. A covering relation is deliberately not transitive, and taking its transitive closure gives you back the order, so the two are opposite ends of the same operation. The spec had one sentence that was true of one of these and was written as though it applied to all four, and the code that read that sentence chose a different member than the code that wrote it.
A claim its own document denies
The third kind is the one I found most uncomfortable. One row asserted the round-trip laws for a lens, which require:
get(put(v, s)) = v
put(get(s), s) = s
A different section of the same document, 130 lines away, states plainly that the two maps do not compose to the identity. Both sentences had been read many times, by me, and never on the same day.
This is the failure mode of a long specification. Contradictions are invisible when the two halves never have to be true at the same moment, and nothing in prose forces that moment to happen.
The four unknowns are not failures
Four rows came back unknown, and keeping that as a separate answer is the part I would defend hardest.
One example: a comparison is total only under a hypothesis supplied by a different layer. Whether the claim holds is not decidable where the claim is written. It is not false, and marking it false would produce a repair for a problem that may not exist. It is also not valid, and calling it valid would launder an assumption into a fact.
Collapsing unknown into invalid is the more tempting direction, because it makes the report look rigorous and gives everyone something to do. It is still wrong. The honest output is a count of decided and a named list of what a decision is waiting on.
Why prose lets this happen
None of these five claims survived contact with a checker, and all of them had survived years of reading. Prose does not force you to name the structure, so "this preserves structure" never has to answer which structure, and the reader supplies whichever one makes the sentence true.
The repair is not to write less precisely. It is to make each precise word carry its obligation in machine-readable form: when the document says homomorphism, something should be able to ask which operation on each side, and then check it.
Two things I keep
A precise word is a promise, and the cost of breaking it is paid by a reader who believed you. If you are not prepared to have "homomorphism" checked, write "encodes" and lose nothing.
Contradictions inside one document are found by evaluation, never by reading. Two statements a hundred lines apart are never in your head simultaneously, so no amount of careful reading brings them together. Something that resolves both at once does it in milliseconds.
Top comments (0)