[ulrikrasmussen]

Proving safety is just a small part of the problem to be solved. The hard part is actually structuring the program such that its correctness can even be formulated as a formal property which can be proved. For a lot of software that alone is highly nontrivial.

[recursivedoubts]

From "No Silver Bullet":

> More seriously, even perfect program verification can only establish that a program meets its specification. The hardest part of the software task is arriving at a complete and consistent specification, and much of the essence of building a program is in fact the debugging of the specification

[986aignan]

On the other hand, proofs sometimes give you more than you'd expect. A proof that the implementation of a function always returns some value automatically proves that there's no arbitrary code execution, for instance.