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.
