Program logic bugs vs input/environmental errors

[Nick Sabalausky via Digitalmars-d]

On 10/04/2014 06:20 PM, Nick Sabalausky wrote:
> 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.)
>

And the "specification" itself may have flaws as well, so again, there 
are NO guarantees here whatsoever. The only thing proofs do in an 
engineering context is decrease the likelihood of problems, just like 
any other engineering strategy.