Believe me, I take Dijkstra's message to heart. And a quality test suite can reify the decisions of a formal specification as expressed in PTS or some other suitable abstraction. Think more here's the proof, more or less rigorous as circumstances suggest reasonable, and here's some tests that capture as much of that in code as practicable to help give us some further confidence that we didn't err in our manipulations.
That's a category error. The formal spec isn't a proof, it's what is to be proven. Without a spec the notion of programming errors has no formal meaning. In that case, the complaints about the bug are always with respect to pleasantness. Given a formal specification, it's possible to write a program that will reliably satisfy that specification. And the tooling is better than ever. The Dafny language out of Microsoft Research is one interesting example. One can also do it by hand, possibly using an SMT solver to check one's work.
User23|3 years ago
pydry|3 years ago
User23|3 years ago