Program logic bugs vs input/environmental errors

[Ola Fosheim Grostad via Digitalmars-d]

On Saturday, 4 October 2014 at 22:24:08 UTC, Nick Sabalausky 
wrote:
> 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.

Machine validated proofs guarantee that there are no bugs in the 
source code for any reasonable definition of "guarantee". There 
is no reason for having proper asserts left in the code after 
that.

If the specification the contract is based on is inadequate, then 
that is not an issue for the contractor. You still implement 
according to the spec/contract until the contract is changed by 
the customer.

If an architect didn't follow the requirements of the law when 
drawing a house, then he cannot blame the carpenter for building 
the house according to the drawings.