Comment by andai
8 hours ago
I had a funny experience recently, during a vibe coding bender. This was a few weeks ago when these very impressive new models came out, a whole new class of intelligence and autonomy! So I wanted to see how far I would get, letting the computer handle all the details.
Eventually I did take a look at all the new code, and found that one of the main features had been implemented completely backwards, in a way that was pointless and completely defeated the purpose.
(An LLM also pointed that out, so I guess it must have been a different one which implemented it? I'm trying to get them to sign their names in the commits...)
These new models are very thorough and responsible however, so of course it had written a copious number of tests, and of course all the tests passed! I found this very amusing. It had diligently proven the correctness of the incorrect functionality!*
I've been thinking about how cool it is the AI can assist with writing proofs now, and how we can use this new ability to boost the correctness of our code. It later occurred to me, however, that formal verification would not have helped in this case. It would have just formally verified that the wrong thing was correct!
--
*Yeah I know tests prove the presence of bugs but not their absence. Couldn't think of a better way to phrase that though.
I had a college professor do the exact same thing in class: he made a fairly subtle mistake formalizing his specification, and thus his proof was perfect but did not solve the actual problem he was trying to address.
He was a mathematician and was convinced that formal methods were the future of software engineering. He also loved handwaving that due to Godel's incompleteness theorem, humans were necessary to introduce creative insights (new axioms) that computers would never be able to do.
I eventually obtained top marks both semesters and left convinced that formal methods are a waste of time in >99% of the cases.
> An LLM also pointed that out, so I guess it must have been a different one which implemented it?
Or the same one a minute later. LLMs are the software equivalent of Patagonian weather.
re "An LLM also pointed that out, so I guess it must have been a different one which implemented it?" - no, there is no correlation between whether the same LLM is used and whether it can find errors.