alt Hacker NewsHow 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.