What machine proofs do is concentrate the risk of errors on the proof checker. That is great if your proof checker is reliable, and catastrophic if it is unreliable. Fortunately, proof checkers need not be complicated; you only need a small kernel, from which you can build the rest of the theory.

The other issue is usability. Coq is awesome, but proving something more complicated than basic arithmetic results is hard to do. Likewise with ACL2, PVS, and similar systems. It is getting better, but we are still not quite there.

Well there was some mention.

> We can probably add software to that list: early software engineering work found that, dismayingly, bug rates seem to be simply a function of lines of code, and one would expect diseconomies of scale. So one would expect that in going from the ~4,000 lines of code of the Microsoft DOS operating system kernel to the ~50,000,000 lines of code in Windows Server 2003 (with full systems of applications and libraries being even larger: the comprehensive Debian repository in 2007 contained ~323,551,126 lines of code) that the number of active bugs at any time would be… fairly large. This lead to predictions of doom and spurred much research into automated proof-checking, static analysis, and functional languages

Of course, you need to be pretty confident in your proof-checker. If we aren't totally sure about machine-proof methods, then we comback to the "Doomsday hypothesis" at the end of the article, where many results are invalidated at once.