Program logic bugs vs input/environmental errors

[Nick Sabalausky via Digitalmars-d]

On 10/04/2014 03:57 PM, Ola Fosheim Grostad wrote:
>
> A validated correctness proof ensures that the code follows the
> specification, so no bugs.
>

The day we can guarantee a correctness proof as being perfectly sound 
and...well...correct is the day we can guarantee software correctness 
without the formal proof.

Proofs are just as subject to mistakes and oversights as actual code. 
Proofs deal with that via auditing and peer review, but...so does 
software. It sure as hell doesn't guarantee lack of bugs in software, so 
what in the world would make anyone think it magically guarantees lack 
of mistakes in a "proof"? (A "proof" btw, is little more than code which 
may or may not ever actually get mechanically executed.)