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