checkedint call removal

[Timon Gehr via Digitalmars-d]

On 08/02/2014 08:09 AM, Chris Cain wrote:
> On Saturday, 2 August 2014 at 05:32:43 UTC, Timon Gehr wrote:
>> Well, if there is no proof of something, how can I claim it can be
>> proven? In fact, in my past life, when somebody told me something like
>> '...and actually one _can prove_ that any non-planar graph contains
>> either a K_5 or a K_{3,3} as a minor', then this invariably meant that
>> there exists a proof, but that they will not tell me the proof now.
>>
>> Words are strange; apparently it is very common that they don't mean
>> similar things to different people. Isn't it possible, that
>> 'verifiable' just has an idiomatic usage that does not represent the
>> obvious meaning derived from 'verify'? Or is 'verify' bivalent like
>> that as well?
>
> It seems to be exactly as Tofu suggested. I don't really know exactly
> how to explain to you that the concept of verifiability/falsifiability ...

I actually knew and used falsifiable in this way you suggest. :)
I still don't think that if I falsify a statement, that I might actually 
have proven it true though.

>
> http://en.wikipedia.org/wiki/Falsifiability
>
> ^^ See?

"A statement is called falsifiable if it is possible to conceive an 
observation or an argument which proves the statement in question to be 
false."

If we have proven the statement true, we won't readily deem it possible 
to conceive an observation or argument which proves the statement in 
question to be false.

> It's an important part of science that there is the possibility
> of proving it false.

Not exactly. The article is stating that it should be conceivable that 
there might be an argument or an observation proving it false. But that 
often holds simply because we cannot prove properties of reality to 
hold. It is conceivable that gravity will not exist tomorrow and this 
would falsify many theories of physics. I don't really believe that this 
will happen, but it is conceivable.

> That *doesn't* imply it *is* false, though.
> Likewise for verifiability (they're really just synonyms, which should
> really show you that there actually existing both a proof for truth and
> falseness doesn't make sense)
>
> http://www.synonym.com/synonyms/falsifiable/ -> verifiable is a synonym.
> ...

Thanks! My hypothesis that verifiable/falsifiable are just idioms not 
extending to verify/falsify is not shattered by this though.

> .. I knew the dictionary understanding but simply separated the concepts in
> my head before. I thought of the assert in programming languages as you
> currently do. However, this thread has shown me that they were always
> intended to be the same, and it's significantly clarified (for me) where
> I would use assertions and where I'd use enforcements, for instance (the
> boundry has always been pretty fuzzy to me... "use asserts for the
> purpose of program bugs" has always been somewhat unclear).
> ...

I would actually agree with applying this reasoning for usage to 'old' 
assertions.

> ...
>
> Sure. A bit of a different flavor, but essentially the same. Incorrect
> statements make incorrect program behavior (in the case of assert, I
> think understanding the real meaning behind it will make it far easier
> to reason about ... "UB" isn't quite accurate as the meaning behind what
> you say has a clear implication of what type of behavior will follow,
> it's just that currently the optimizer doesn't do all it could do)
> ...

The type of behaviour that will follow (or indeed, precede the 
assertion) is dependent on whether or not the assertion may fail. If it 
may fail, UB will come and maybe eat your program, and chances are you 
won't notice immediately what happened. I guess we just disagree on the 
importance of this point.

> ...
>
> I'd like to reiterate that I think it would be better if the compiler
> COULD prove some assertion impossible at compile time, then it should.
>
> e.g.
>
> ```
> int x = 1;
> assert(x != 1);
> ```
>
> ... It'd be reasonable for this to fail to compile. Frankly, this could
> unify static assert and assert (though, I'm not sure if I'd feel
> comfortable with this... I'd, after all, prefer a static foreach and I'd
> also like to keep my static ifs because I'd like to enforce that these
> things are always handled at compile time).

It is not so clear where to draw the boundaries. In some languages you 
may need to prove the assertion true in order for it to pass the type 
checker.