3 ms·

Yup. This shows why we need languages that are more amendable to formal methods. Proving stuff requires you to write short code that is obviously correct. For

Yup. This shows why we need languages that are more amendable to formal methods. Proving stuff requires you to write short code that is obviously correct. For most programs, an 'informal' proof would be a huge improvement already. The effort you have to put in non-formal proofs is much lower, but the main drawback is that they are not checked, so you might make mistakes in the proof (on the other hand, you can make mistakes in the specification as well). The holy grail would be formal methods that work mostly like informal proofs. With todays methods you would only prove the smallest, most critical parts of the code correct.

zozbot234 7y ago
If you're going to write a formal spec in the first place, you can then "fuzz" the code against the spec, or parts of the spec against itself. I.e. try to find an automated refutation as opposed to a proof. Model checkers work according to this principle, and I assume that the combination of "informal" proof and automated model checking can be especially helpful for suitably-sized systems. Either one of these without the other seems a bit harder to take seriously.