[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.