On Saturday, 2 August 2014 at 21:36:11 UTC, Tobias Pankrath wrote:
Don't you agree, that a program that throws AssertError in non
-release* build is broken?
* this is not the opposite of debug
Let's go to the definitions:
Total correctness:
The program can be proved to always terminate normally and return
the correct result.
Total correctness is extremely difficult to achieve on a regular
computer.
Partial correctness:
The program can be proved to always return the correct result if
it terminates normally.
Partial correctness is what you should aim for. What goes on if
it does not terminate depends on many factors. E.g. the FDIV bug
in the Intel CPU:
http://en.wikipedia.org/wiki/Pentium_FDIV_bug
The FDIV bug is a good example that extensive testing is not
enough and that you need either exhaustive testing or formal
proofs to assert correctness.
Equally clearly, the FDIV bug is not the result of an incorrect
program. It is the result of an incorrect "axiom" in the CPU (the
execution environment).
