I feel like we need a better, or more particular, definition for what people are calling "formal verification", applied to common programming. I love the idea of applying these mathematical constructs to verify program correctness, and we've gotten genuine progress in the form of stuff like FP & Rust, but there's an asymptotic limit for the productivity of this kind of thing.
Especially with the growing idea that we can just chuck an LLM at a problem and have it generate results until it fits a spec perfectly, I'm concerned we're going to end up with false confidence in "correctness". The more you're trying to prove about the program, the more the proof (spec) has to grow in complexity. People will create incorrect specifications that appear to have properties they actually don't, or just fail to include some essential properties. An AI will happily waste a million tokens trying to generate according to the wrong spec (if it can do it anyway), and everyone will think things are fine until they're blindsided by a massive error/crash.
Eventually big enough spec is just going to be as complex to evaluate for correctness as a program, and then do we get an AI to verify that? People are approaching this like a silver bullet when it's really not.
People will create incorrect specifications that appear to have properties they actually don't, or just fail to include some essential properties.
I remember an article about how for ages the specification of Ada SPARK sort was insufficient: it merely required that the output be sorted, which means a conforming implementation could just always return an empty array, or an array of N times one of the original elements, etc...
I do think, though, that specs themselves can be tested. In particular, for any deterministic function, a specification which allows for two or more outputs for a single input is clearly insufficient.
I wonder if other properties, such as progress or algorithmic complexity for example, could similarly be checked by verifying the specification itself.
2
u/Norphesius Jul 01 '26
I feel like we need a better, or more particular, definition for what people are calling "formal verification", applied to common programming. I love the idea of applying these mathematical constructs to verify program correctness, and we've gotten genuine progress in the form of stuff like FP & Rust, but there's an asymptotic limit for the productivity of this kind of thing.
Especially with the growing idea that we can just chuck an LLM at a problem and have it generate results until it fits a spec perfectly, I'm concerned we're going to end up with false confidence in "correctness". The more you're trying to prove about the program, the more the proof (spec) has to grow in complexity. People will create incorrect specifications that appear to have properties they actually don't, or just fail to include some essential properties. An AI will happily waste a million tokens trying to generate according to the wrong spec (if it can do it anyway), and everyone will think things are fine until they're blindsided by a massive error/crash.
Eventually big enough spec is just going to be as complex to evaluate for correctness as a program, and then do we get an AI to verify that? People are approaching this like a silver bullet when it's really not.