The original study saying formal verification was useless. In Section 6 of this paper [1], Avra Cohn gave a similar reality check when attempting to mechanize a hardware proof. Also, Guttman summarizes here [2] problems with many verification efforts. Finally, Wired has a modern take [3] on debate in 1979 paper by de Millo et al. These collectively represent most of opposition’ points to formal verification of software.
This is great for its description of social process of mathematics, the traditional approaches, and the limitations. I’m probably going to do a takedown of some points in the de Millo et al work at some point because I think the field got far enough to address some of it. There’s still some truth in what they’re saying. Probably best to treat new approaches as something different from traditional math with their own goals and expectations.
Any rebuttal of mine would focus on the LCF + de Bruijn approach negating much risk in proof steps, the high-level languages/frameworks that were built to make it easier (not easy), the fact that many people are doing what they suggest they won’t, the examples corroborating reliability benefits, and something exploring vetted theorems vs vetted verified components which I think are similar in how they’re used.
The risk that they predicted best was trusting verified components so much they didn’t include other checks: many ended up doing that. Good news is we have ways to do assurance in depth for those that are willing. Essentially, we just combine different methods of risk mitigation instead of relying on any one too much. Also, always have field updates, monitoring and recovery built into the plan for the system.
EDIT: On Lobsters version, Derek Jones added his blog post [4] making similar claims with a number of references. Thursten's "On proof and progress in mathematics" was a great read.
This is great for its description of social process of mathematics, the traditional approaches, and the limitations. I’m probably going to do a takedown of some points in the de Millo et al work at some point because I think the field got far enough to address some of it. There’s still some truth in what they’re saying. Probably best to treat new approaches as something different from traditional math with their own goals and expectations.
Any rebuttal of mine would focus on the LCF + de Bruijn approach negating much risk in proof steps, the high-level languages/frameworks that were built to make it easier (not easy), the fact that many people are doing what they suggest they won’t, the examples corroborating reliability benefits, and something exploring vetted theorems vs vetted verified components which I think are similar in how they’re used.
The risk that they predicted best was trusting verified components so much they didn’t include other checks: many ended up doing that. Good news is we have ways to do assurance in depth for those that are willing. Essentially, we just combine different methods of risk mitigation instead of relying on any one too much. Also, always have field updates, monitoring and recovery built into the plan for the system.
EDIT: On Lobsters version, Derek Jones added his blog post [4] making similar claims with a number of references. Thursten's "On proof and progress in mathematics" was a great read.
[1] http://www.cl.cam.ac.uk/archive/mjcg/papers/AvraProofPaper.p...
[2] http://www.cypherpunks.to/~peter/04_verif_techniques.pdf
[3] https://www.wired.com/2013/03/computers-and-math/
[4] http://shape-of-code.coding-guidelines.com/2018/02/19/mathem...