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.
-
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.
@david_chisnall Nah but that means you have to think. Nowadays you just throw wild ideas out and see what sticks, maybe the machine will "think" for you even. Bleh.
-
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.
@david_chisnall people dont notice, because they are used to write specifications in the form of telling others what to do.
They still should talk about this part more though, as they are often very terrible in it.For the fun part, many of the verification steps are also done directly or indirectly by generated code. So it needs a lot of manual testing.
A bit like trial and error programming one is doing in the first years of learning....
-
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.
@david_chisnall (I know this isn't quite what you're discussing, but I feel the parallels are easy to make.)
-
@david_chisnall Nah but that means you have to think. Nowadays you just throw wild ideas out and see what sticks, maybe the machine will "think" for you even. Bleh.
@mathieu @david_chisnall Nevermind that _we_ (huh?) are all fanatical _technophobes_ standing in the way of progress or some such!
-
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.
@david_chisnall I haven't fully thought this through so maybe I'm wrong, but I feel like a _full_ correct specification of how a program should work has to be on par in complexity with "just" writing the program?
-
@mathieu @david_chisnall Nevermind that _we_ (huh?) are all fanatical _technophobes_ standing in the way of progress or some such!
@seufz @david_chisnall Yup, I'm a bit removed from all of this crazyness (by choice), I recently stumbled upon some "pro AI" communities and indeed they see "us" (wtf there is no us/them but okay) as technophobes trying to shut down everything out of fear. The world is wild.
-
@david_chisnall I haven't fully thought this through so maybe I'm wrong, but I feel like a _full_ correct specification of how a program should work has to be on par in complexity with "just" writing the program?
@SonnyBonds @david_chisnall A formal proof of the existence of a fully specified program is equivalent to code to implement that program c/o Martin-Löf type theory and others, but writing such proofs is harder than writing correct code usually.
-
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.
@david_chisnall > And why is writing a formal specification believed to be easier than writing code?
Code is just whatever format it takes to specify for a computer what it should do, in an unambiguous way. We simplify the code by making nonsensical things inexpressible. If a formal specification was easier enough to write, then that would *be* the code. Plus some synthesis tool to convert it to an executable.
-
@david_chisnall I haven't fully thought this through so maybe I'm wrong, but I feel like a _full_ correct specification of how a program should work has to be on par in complexity with "just" writing the program?
Often a bit simpler. The specification of a sorting algorithm, for example, may just be a post condition that, for all indexes n and n+1, the value at n+1 is greater than or equal to the value at index n. That’s simpler than, say, a quicksort implementation. But the proof that quicksort satisfies this specification is often more complex than the quicksort.
-
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.
@david_chisnall you'd think that none of these people know what the tradeoffs of an abstraction layer are.
What you said... if this were easy formal verification would already be ubiquitous. The whole point of constantly advancing our programming languages is to have more refined specifications that allows everything to be reused more easily and more broadly.
Simply using an LLM as an abstraction layer doesn't eliminate the chaos underneath it all. It just pushes it farther away. That can't see how that works out in the long run.
If LLMs rule the world and nobody is guiding the development of underlying specifications, wouldn't we eventually end up with one of two extreme undesirable outcomes?
1) A programming landscape that's entirely standards free.
2) A programming landscape that's homogenized as diversity and critical edge cases get factored out by LLMs as undesirable.
-
R relay@relay.publicsquare.global shared this topicR relay@relay.an.exchange shared this topic
