3 ms·
It's a common idea, all the way back to Hoare logic. There was a time when people believed in the future, people would write specifications instead of code. Th
by InkCanon 1y ago
It's a common idea, all the way back to Hoare logic. There was a time when people believed in the future, people would write specifications instead of code.
The problem with it takes several times more effort to verify code than to write it. This makes intuitive sense if you consider that the search space for the properties of code is much larger than the code for space. Rice theorem's states that all non trivial semantic properties of a program are undeniable.
- Smaug123 1y agoNo, Rice's theorem states that there is no general procedure to take an arbitrary program and decide nontrivial properties of its behaviour. As software engineers, though, we write specific programs which have properties which can be decided, perhaps by reasoning specific to the program. (That's, like, the whole point of software engineering: you can't claim to have solved a problem if you wrote a program such that it's undecidable whether it solved the problem.) The "several times more effort to verify code" thing: I'm hoping the next few generations of LLMs will be able to do this properly! Imagine if you were writing in a dependently typed language, and you wrote your test as simply a theorem, and used a very competent LLM (perhaps with other program search techniques; who knows) to fill in the proof, which nobody will never read. Seems like a natural end state of the OP: more compute may relax the constraints on writing software whose behaviour is formally verifiable.
- deterministic 1y agoUsing a LLM to generate the proofs from a spec and verify it (OK/Error) would make it much faster.