assert semantic change proposal

via Digitalmars-d digitalmars-d at puremagic.com
Wed Aug 6 13:57:38 PDT 2014


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.


More information about the Digitalmars-d mailing list