Comment by amelius
21 hours ago
Having not been formally verified, almost all software today feels cheap. Maybe an AI can change that at some point.
21 hours ago
Having not been formally verified, almost all software today feels cheap. Maybe an AI can change that at some point.
By Dijkstra's standards, we've been vibe coding for an entire century!
I 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.
Of course, but that doesn't mean formal verification isn't a huge step forward.
Yay let’s lock ourselves into the formal verification toolsets, so that we can never use new language features again.
When 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?
Would you board a plane designed by AI that no engineer had ever looked at?
Or some engineer did give a cursory glance at and stamped it with LGTM?
Yes. Correct software is more important than developer convenience.
OR 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.
Both this and the parent takes are exceedingly odd - don’t you think that it’d lead to the language features also just getting the same proofs, as well as better libraries and frameworks? And do you not think that this would also lead to the LLMs both outputting better code since they’d be trained on the verified stuff and also because we’d have tooling to let agent loops autonomously resolve most of the issues with what they output?
I’d rather wait 5-10 years for a stdlib way of handling JSON, XML, YAML, TOML and other formats than using unproven libraries made with unserious practices that have edge cases. The same applies for processing requests, doing any sort of multiprocessing, DB interaction, validations, hell even any and all front end work all they way down to CSS. Don’t even get me started on desktop and server software and OS stuff.
Maybe then software engineering can be treated like real engineering.