On Monday, 28 July 2014 at 16:32:46 UTC, Daniel Murphy wrote:
Yes. I think you'll find advanced optimizers are already doing this sort of thing to your code, when it decides code is unreachable.
The problem is that the code is not unreachable when you compile with -release.
Sure, we could add a new construct (ie 'assume') to the language, and use that to pass information. But are they really different?
The difference is that if you assume(), then you have to formally prove it to hold. That means it cannot be allowed to contradict the program code.
It is very important to keep the provided facts and the derived properties separate.
Assert says 'the program is in error if this is not true'.
enforce() says: always runtime check this (?) assert() says: this ought to hold when I do testing assume() says: I have proven this to hold prove() says: don't generate code until you can prove this to hold
-release says 'compile my program as if it has no errors'.
-release says: compile my program without runtime checks for correctness
-no-assume might say: ignore all assumptions, I don't trust myself -assume-is-assert(): turn assumptions into runtime checks etc.
These two combined give the compiler a huge amount of power.
Yes, if used carefully, but the language and/or compiler have to treat user provided facts differently than derived knowledge that originates within the executable code. assert() is not really for providing facts, it is for testing them. So the threshold for providing an assertion is low if it is completely free of side effects (in release), but the threshold for providing an assumption should be very high.
