5 ms·

I think you might enjoy this paper, I did: http://www1.cs.columbia.edu/~angelos/Misc/p271-de_millo.pdf http://www1.cs.columbia.edu/~angelos/Misc/p271-de_millo.p

• ScottBurson 9y ago
  I think this paper is quite wrong, and has already been shown to be wrong by all the people who have successfully applied formal methods to their projects. We believe that, in the end, it is a social process that determines whether mathematicians feel confident about a theorem — and we believe that, because no comparable social process can take place among program verifiers, program verification is bound to fail. This overlooks the fact that the verifiers aren't black boxes; people trust the TLA+ tools and Coq and Isabelle and PVS because the principles by which they work are well understood, and on top of that, these tools are all open source. (If someone developed a closed-source verifier, they could still leverage this trust by making their verifier output proofs in a format that could be checked by one of these.) So while the individual proofs generated in a software verification are probably not going to be checked socially -- they're mostly just not interesting enough -- there is still a social process operating at the meta-level that gives us confidence in them.