On Sunday, 3 August 2014 at 21:36:44 UTC, Timon Gehr wrote:
>
>>> Again, in other cases, the -release program will operate as expected.
>>
>> If I've grasped your point in the previous reply, yes, maybe.
>> ...
>
> Ok. This was Johannes' point.

Taken, thanks for the explanation: I agree that you both that optimising on a wrongly written assert could turn in code breakage under the new '-release' semantic.

---
Paolo

Just clearing up an old post that bugs me:

On Friday, 1 August 2014 at 10:24:26 UTC, Ola Fosheim Grøstad wrote:
> An assert does not take a predicate.

That was true, as far as D asserts go... but this is also confusing since "predicate" and "assert" can mean different things in different contexts and what I wrote here was a really bad way of putting it:

> bool test(bool x) {return x || !x} // predicate
>
> test(x) for all x in {true,false} // proposition

The terminology used above is likely to confuse an unsuspecting reader, so to make it more clear:

Proposition, as in propositional logic (zeroth order logic): Logic statements that allows us to reason about individual boolean constants without necessarily knowing their actual value. I.e. we list each one "test(true) && test(false)", "test(X)&&test(!X)" or just "test(X)" etc.

Predictate, as in predicate logic (first order logic): statements that extends propositions by expressing possibly infinite sets of values (e.g.  "f(x) holds for all integers lager than 3" or "there exists at least one integer x for which f(x) evaluates to true"). In essence it allows you to write an and-expression or or-expression with an infinite number of terms.

But in C++/D etc "predicate" usually is just used to refer to a boolean pure function in the language. Which is reasonable since there is no support for propositional or predicate logic. A D assert is only evaluated when we know the actual boolean value, which is sound.

So what I meant in this thread is that a compiler should not conclude that an assert holds as if it was a proposition. I.e. turn run-time assertions into compile-time assumptions.

In the context of verification a predicate, in the sense of having for-all or there-exists quantifiers, can be tricky since we may actually run into a statement that may always be true, but for which no known proof exists. (And there we enter the whole domain of the halting problem etc, which essentially boils down to there being more problems than proofs.)

Terminology is such a nuisance...

On Tuesday, 23 May 2017 at 08:41:12 UTC, Ola Fosheim Grøstad wrote:
> But in C++/D etc "predicate" usually is just used to refer to a boolean pure function in the language. Which is reasonable since there is no support for propositional or predicate logic. A D assert is only evaluated when we know the actual boolean value, which is sound.

As an example, if D had support for propositions we would be able to instantiate templates with boolean parameters using expressions like:

f(int x){
   … sometemplate!(x*x >= 0) …
}

with x being unknown at compile time.