checkedint call removal

[Ola Fosheim Grøstad via Digitalmars-d]

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...