I accidentally read LinkedIn again and lots of people are talking about the flow of writing code with an LLM and then using a feedback loop with formal verification to reject incorrect implementations.
On the surface, this seems sensible: LLMs can produce kind-of correct (or, at least, correct-looking) code rapidly, verification tools can tell you if it’s correct and you can just keep exploring the design space until you find something correct.
But the bit no one is talking about is: who writes the specification, which must be sufficiently detailed that it can reject incorrect things (including thins in the wrong complexity class, so you don’t accept when the LLM writes a factorial complexity algorithm where a linear one would work)? And why is writing a formal specification believed to be easier than writing code? And what tools can take an arbitrary program and prove that it does or does not implement a spec? If these things were all easy, formal verification would already be ubiquitous.
On the surface, this seems sensible: LLMs can produce kind-of correct (or, at least, correct-looking) code rapidly, verification tools can tell you if it’s correct and you can just keep exploring the design space until you find something correct.
But the bit no one is talking about is: who writes the specification, which must be sufficiently detailed that it can reject incorrect things (including thins in the wrong complexity class, so you don’t accept when the LLM writes a factorial complexity algorithm where a linear one would work)? And why is writing a formal specification believed to be easier than writing code? And what tools can take an arbitrary program and prove that it does or does not implement a spec? If these things were all easy, formal verification would already be ubiquitous.
3
