checkedint call removal

[via Digitalmars-d]

On Thursday, 31 July 2014 at 05:56:31 UTC, Walter Bright wrote:
> On 7/30/2014 10:16 PM, bearophile wrote:
>> Walter Bright:
>>> Show me a piece of code with different behavior. Start with 
>>> the array bounds
>>> thing.
>> People have already shown you code that behaves differently 
>> with assert and
>> assume.
>
> I'd like to see what you are saying is different in a real 
> example.
>
>
>> But you have redefined "assert" to mean a mix of assume and 
>> assert.
>
> I haven't redefined anything. It's always been that way. It's 
> used that way in C/C++ (see your Microsoft C++ link).

No.

This is safe:

assert(x) {
    if(!x) halt();
    assume(x);
}

This is not safe:

assert(x){
   assume(x);
}


You need to underestand what can be proven with Hoare logic. The 
optimizer is free to do anything you can do with it.

A program + libaries contain millions of statements. Each and 
every of those statements is taken as something close to an axiom 
or multiple axioms. Basically your program contains millions of 
implicit assumes() that are internally consistent.

Then you add thousands handwritten axioms of assume().

true == false IFF a single of those axioms contradicts another 
axiom either provided implicitly by the program/optimizer or 
explicitly by the user.

That means any boolean expression in your program+libraries can 
be proven true or false randomly with a probability close to 100%.

That means you cannot do heavy duty optimization at all! Because 
the probability of no axioms contradicting each other is very 
close to 0%!

Please note that you can infer true==false if there is even the 
tiniest teeny weeny sign of contradiction in any pair of axioms 
picked from the millions upon millions of axioms provided. Even 
if that axiom is derived from a statement deep down in some 
library that most likely will never execute.

assume(X) provides axiom X

assert(X) provides theorem(X) to be proven

You cannot mix those two. That is disaster.