What a Proof Covers

Lately I hear a version of this often: models find bugs faster than people can fix them, so write the code in Lean, prove it, and it will be secure.

Part of that is right. A proof covers every input, which no test does. The rest skips over what the proof is a proof of. In the next couple of posts, I’m going to take one small rule through an example test, a property test and a proof, and write down what each one established. Follow along and you’ll:

• see the same rule checked for one list, for a thousand lists, and for every list
• read a complete Lean proof by induction, one step at a time, with no background in Lean assumed
• see that proof go through for a function that is plainly wrong, and see which stronger statement catches it
• see what a proof about a Lean definition says about C# and Go code, and about a Lean program that also does I/O

The rule is deliberately tiny: reversing a list twice gives back the list. Nothing about it is hard, which is the point. With the difficulty removed, what is left is the difference between the three kinds of evidence.

I’m not arguing against proofs. I have spent years on property-based testing and on fuzzing, and a proof is strictly stronger than both for the statement it proves. The argument is about that last clause.

Here’s a list of posts to follow:

• One List, a Thousand Lists
• Every List
• The Theorem Holds for the Wrong Function
• The same three tools on a real bug (to come)

Examples are in C# and Go, with Hedgehog and testing/quick for the property tests, and Lean 4 for the proofs.

Entry dated July 10. The posts were written in November, and the code in them was run then, with Go 1.27, Hedgehog 2.0.4 and Lean 4.35.