alt Hacker News> As the verification process itself becomes automated, the challenge will move to correctly defining the specification: that is, how do you know that the properties that were proved are actually the properties that you cared about? Reading and writing such formal specifications still requires expertise and careful thought. But writing the spec is vastly easier and quicker than writing the proof by hand, so this is progress.
Proofs never took off because most software engineering moved away from waterfall development, not just because proofs are difficult. Long formal specifications were abandoned since often those who wrote them misunderstood what the user wanted or the user didn’t know what they wanted. Instead, agile development took over and software evolved more iteratively and rapidly to meet the user.
The author seems to make their prediction based on the flawed assumption that difficulty in writing proofs was the only reason we avoided them, when in reality the real challenge was understanding what the user actually wanted.
Replies
And yet code is being written and deployed to prod all the time, with many layers of tests. Formal specs can be used at least at all the same levels, but crucially also at the technical docs level. LLMs make writing them cheap. What’s not to like?
The thing is, if it takes say a year to go from a formal spec to a formally proven implementation and then the spec changes because there was a misunderstanding about the requirements, it's a completely broken process. If the same process now takes say a day or even a week instead, that becomes usable as a feedback loop and very much desirable. Sometimes a quantitative improvement leads to a qualitative change.