I think that the classic ironical demonstration of the limits of proof systems comes up with the fact that CoqIDE 8.7.1 crashes immediately on OSX if you try to cut or paste anything.<p>The problem, it turns out that they included a new version of OCaml which was incompatible with the older version of GTK that was being used. Result: crash due to seg fault.<p>We really need both proofs and pragmatics. Proofs can give us confidence in the fundamentals when used appropriately for the processor, or for consensus algorithms like Raft, or key parts of the OS. Tests and statistical analysis can give us confidence that we haven't overlooked something crucial.<p>Some systems obviously aren't very appropriate for formal methods (take machine learning, for instance, there can be no formal spec for what a fraud looks like). There statistics and testing will have to suffice because we have clear value on average even if we cannot formally guarantee the system.<p>Other systems are much more appropriate for formal methods. I should hope that a heart monitor, CPU, voting machine or aircraft flight management system will have substantial amounts of formally proved code (I know that I am dreaming with the voting machines; let's settle for getting it down on paper). I don't want to collect a statistical sampling of whether an airplane works as we iteratively work out the bugs and specs in an agile fashion.