On 10/4/2014 10:24 PM, Ola Fosheim Grostad wrote:
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.
Carpenters can be liable for building things they know are wrong, regardless of
what the spec says.
