Hacker Newsnew | past | comments | ask | show | jobs | submitlogin

Why not? Because provably correct software is not necessarily correct software. One of the biggest classes of defects in programs is missing details in specifications, and provable correctness against the wrong specification doesn't help with that problem at all.

Provable correctness is one technique in software development, it's not the only technique nor even the most important technique nor even a required technique.



Yep.

Provable correctness can be useful iff you have a formal specification, and iff that formal specification is more likely to be a correct reflection of the requirements than the code + some tests.

While there are times when that's the case, those are rare.




Guidelines | FAQ | Lists | API | Security | Legal | Apply to YC | Contact

Search: