On Wednesday, 6 August 2014 at 17:36:00 UTC, Artur Skawina wrote:
if (0) assume(0);Yes, `assume` could be defined in a way that would make this always a compile error. But then `assume(0)` would be useless.
I don't think so. It makes a lot of sense to halt compilation if you from templates or other constructs emit assume(true==false) or assert(true==false) or any other verification-annotation that contradicts predefined language axioms in a way that the compiler can detect at compile time. Otherwise you risk having "unreachable" unintended in generic code.
It also basically gives you a very limited version of a theorem prover and thus the capability of doing real program verification. This should be extended later so that the language supports program verification within it's own syntax.
I also dislike this kind of special casing in general. Semantics should be consistent. assert(false) and assume(false) are aberrations, I totally agree with what bearophile has previously stated. Making formal program verification impossible by odd special casing (C mal-practice) is counter productive in the long run.
