On Tuesday, 29 July 2014 at 06:35:06 UTC, Daniel Murphy wrote:
The idea is you test your code with assertions enabled, and
then only use '-release' when you are sure your program
functions correctly.
It never works correctly, until proven correct formally with an
automated theorem prover. As I pointed out, even if you only make
a mistake in 1 out of 1000 asserts (mistake being having an
assert not matching the program logic) you still get a 40% chance
of complete failure. No programmer is capable of such a low error
rate either.
Please note that is not sufficient for the asserts to follow the
specification, they must also not contradiction the logic
embedded in the program. One contradictive theorem in the
optimizer and it will generate garbage.
For this to work without formal proofs you will have to:
1. do exhaustive unit-testing of all input, function by function.
2. the function has to be fully deterministic (no
multi-threading, floats, timers etc)
The key to verifying correctness is that you have 2 separate
formulations of the same logic:
1. specification
2. implementation
You compare the implementation to the specification. That is what
verifying correctness is.
If you use the specification for implementation (which is what
conflating assert() with assume() is), then you only have the
implementation and all discrepancies will lead to contradictions
or other flaws that will lead to illegal code-gen. And undetected.
This thread gives me an headache… :-(
