checkedint call removal

[via Digitalmars-d]

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… :-(