As a huge believer in formal methods, this statement should _also_ be tempered somewhat. Formal proof is a great technique, but it's incredibly dependent on getting your specs right, which is very hard to do.
As an example, CompCERT is a formally verified C compiler, and it's had a couple bugs as a result of their specification of the underlying hardware being wrong.
As an example, CompCERT is a formally verified C compiler, and it's had a couple bugs as a result of their specification of the underlying hardware being wrong.