How do you know any test is checking what you want? You either review it, and/or you run the test on things you know are good and also things you know are bad.
How do you know any test is checking what you want? You either review it, and/or you run the test on things you know are good and also things you know are bad.
Well they are much harder to read than tests.
I was going through an experiment trying to spec out a simple caching system in Lean. I was getting Gemini to help me run through doing this, step by step. At one point it writes out this statement with a proof to show something, the specifics of which I forget, but it was some simple property of the cache. I stare at it for a while thinking to myself this can't be right, it was some sort of plain tautological statement that didn't really say anything, like saying 1 = 1.
I give it to Opus 5.5 and it basically confirmed my gut feeling that it was useless.
I'd like to rely more on formal verification. I like the idea of starting out with specs in a formal setting and designing software that way. The problem is it's hard to do right, and my point is even with AI, it's hard to do right.
I fully agree it’s harder to read. I do chip design and I feel like formal is more common in this area, but I generally restrict it to very simple properties that are easy to understand without having to mentally solve a sudoku puzzle.
It’s to easy to write an assertion that looks like it checks what you want it to, and gives you a false confidence when it passes, only to figure out after a field failure that it wasn’t checking what you thought at all.
But I’d pay for a commercial set of properties and assertions that had guarantees, and not worry about their complexity. For something standard like cache protocols and bus protocols.
Other cases it needs to be pretty straightforward to grasp by a peer reviewer in minutes, or it’s not worth it.
But when you can hit the sweet spot, a set of easily understood properties (or complex but trusted properties), formal can save massive amounts of time.
That's the nice thing about the approach described in the blog: you use the same Rocq theorem for every binary (it just says "this binary doesn't crash") and then you express the property you want in your language of choice. For example, to prove that your compression algorithm round-trips, you would write something like assert(x == decompress(compress(x))).