3 ms·

Beware of bugs in the above code; I have only proved it correct, not tried it. -- Donald Knuth Code meeting spec doesn't magically make the spec right.

• wiz21c 8y ago
  Is it already the case that a specification good enough to prove a program is bug free is smaller/less complex than the program itself. Because if it is not, then I'd assume the risk of failure in the specification just becomes bigger than in the program itself... So you'd need another tool to prove that the spec is correct...
  • naasking 8y ago
    Or you have the spec written twice, by two independent people and then compare.
    • vinceguidry 8y ago
      SQLite has three independently developed test codebases.
  • vinceguidry 8y ago
    The spec not being right means the human/humans that made it couldn't foresee all possible edge cases. It's not a bad thing for the spec to exceed the size of the program. SQLite does this, with over 700 times more test code than application code. The spec is the human interface to the expected behavior of the program, while the code is the human interface to the actual behavior of the program.