By Dijkstra's standards, we've been vibe coding for an entire century!
replyI had similar thoughts recently, that now that machines are good at writing proofs, this could help with their reliability in software development.
Then I had a funny incident where an LLM implemented a feature completely backwards. Plenty of tests were supplied which demonstrated that the completely broken feature was correctly implemented.
I realized that formal verification would not have helped here, if I had left the task to the machine. It would simply have written a mathematical proof of the correctness of the incorrect feature!
Apparently this is an issue for humans as well, called the "spec gap" or something like that.
It is the reason why user stories were established, so that the person interpreting the spec knows why. Generally speaking this reduces the likelihood of this gap occuring with humans significantly. At least when they're not incompetent.
replyYay let’s lock ourselves into the formal verification toolsets, so that we can never use new language features again.
replyWhen you board a plane, don't you love thinking about how the controllers can make use of the hottest new language features? Perhaps JSON in the stdlib?
replyYes. Correct software is more important than developer convenience.
replyOR new languages and frameworks ever again, since they'll slow down code generation due to lack of training, and from LLM generation standpoint this is a terrible thing to trade off.
reply