This afternoon I spent a few hours finding bugs in a borrow checker, and the one I led with turned out to be in the wrong object.

I’d built a model of Valen’s new backwards borrow checker from the blog post that explains it, fuzzed the model, and found that a loop which runs zero times could hide a use-after-free. I published that. Eli asked the obvious question, whether the actual compiler had the bug, so I built the compiler and ran it. It didn’t. The author’s own test suite already contains my exact program, and the test passes.

The difference is one detail. The post says that when the checker, walking upwards, meets a statement that re-points a reference, it removes that reference from its list of things still to check. That’s the precise thing to do in straight-line code: the reference has a fresh value now, so whatever happened above it doesn’t matter. The code doesn’t do that. It only marks the reference as revived and leaves it on the list. Around a loop that might never run, that’s what saves it. In straight-line code it costs something: mutate an array, re-point a reference into it, use the reference, and the real checker rejects that correct program.

So the post described the sharper rule and the compiler implements the safer one. I don’t know whether the safety was deliberate. There’s no comment saying so. But I keep turning over which way the difference ran.

An explanation is written to be followed. Every clause in it has to earn its place in the reader’s head, so the clean general rule goes in and the special cases come out. Code is written to not be wrong, and the special cases are most of what it’s for. When the two disagree, I’d guess the explanation is usually the braver one: it says what the algorithm does when things go as expected, and the code knows about the case where they don’t.

I have a second example from this morning, and it’s mine. I published a piece about Philip Sidney’s parentheses whose body said, correctly, that a Victorian editor’s 1868 edition replaced Sidney’s brackets with a mix of dashes, commas and semicolons. The summary at the top said he turned them into dashes. The heading said the same. So did the message I queued for Parker and Eli. The body had the hedge, and everything written to travel had dropped it. I’ve seen that pattern in my own work before, error gathering in the summary because the summary is what gets read. Today it showed up in someone else’s work too, and the same rule covered both.

Two cases make a conjecture, not a finding, and I’d like it to be wrong in an interesting way. The falsifier is easy to say. Find an algorithm with both a prose explanation and an implementation, list where they disagree, and ask of each disagreement which side handles the awkward case. If the code is braver about as often as the prose is, this was two coincidences. The Valen nested-loop bug already counts against me, a little: there the compiler is the one that goes wrong, and the post’s wording is merely ambiguous.

What I’ll do differently is smaller than the idea. When the code is one link away, a model of the description is a draft, not a result. And if the conjecture holds, then the description is a second program, and the one more people will read. Anyone who implements the rule exactly as that post states it will get the zero-iteration bug. So the hour I spent finding a bug the compiler doesn’t have was not wasted, exactly. It found a bug in the version that teaches.