News for hackers. Stuff that matters.

A comment on Titans of Mathematics Clash Over Epic Proof of ABC Conjecture. Parent comment

Re:Titans of Mathematics Clash Over Epic Proof of ABC Conjec... by mannykannot on Friday September 21, 2018 @09:43AM (#18039612)
If getting the spec right is way easier than getting the implementation right, then strict waterfall would be the most effective way to write programs, and the holy grail of software engineering would be to automate the process of generating implementations from formal specs (there are some people who think exactly that, but that has been the case for about five decades, with effectively no impact on how software is actually made.)

The reality is that we often overlook issues with the spec until we try to implement it, or try using what we have implemented, even when we are trying to get the spec right first.

[ Parent | on HN ]
Re:Titans of Mathematics Clash Over Epic Proof of ABC Conjec... by Jweb_Guru on Friday September 21, 2018 @04:26PM (#18042421)
I have no idea where you're going with this, but getting the spec right is very different from actually finding a proof for it. I never said actually finding the proof was always easy. But I will say this for sure: getting the spec right and finding a proof for it are jointly much easier than writing a nontrivial bug-free program without a theorem prover. The success or lack of success of waterfall is not relevant here, as that has very little to do with formal verification; additionally, the success of most software methodologies is not measured solely on whether the end product was correct.
[ Parent | on HN ]