checkedint call removal

[Chris Cain via Digitalmars-d]

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 does not mean that something will 
verify as true or be falsified just to assert that they have an 
ability of being shown to be false or shown to be true (that is, 
there needn't be a proof in hand or even discovered, just that 
some proof could be written about it's truth or falseness, even 
if it has never been discovered).

In the world of science in general, "falsifiability" is clearly 
used for any research. It means "able to be proven false", of 
course, but if that implied it wasn't true, then it would mean 
that all science is false which is truly a bizarre conclusion.

http://en.wikipedia.org/wiki/Falsifiability

^^ See? It's an important part of science that there is the 
possibility of proving it false. 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.

> For me, having them double checked is the main motivation for 
> writing down assertions. I like failing assertions when they 
> occur. They often almost immediately tell me what I screwed up, 
> or which prior assumptions no longer hold and which code 
> therefore I might need to modify in order to complete the 
> implementation of a new feature. I personally don't want the 
> compiler to trust me regarding those issues, and that's the 
> whole point. This is how assert works in other languages and 
> also how it works in current D compilers. However, whenever I 
> write an assertion down, it is still a statement of 
> fact/opinion/whatever, and more importantly, I feel strongly 
> about that it should be true.
>
> I don't think that if I had looked up 'assert' in a dictionary, 
> I would have recognised an opposition between the definition in 
> the dictionary and the 'old' semantics as described above.

I could see that. That said, I was on the opposite side of the 
fence. 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 guess not everyone knew and understood the dictionary 
definition, so it seems that my point wasn't originally helpful.

> Note that it might just as well be a command that makes the 
> program make a statement of fact.

That's pretty much exactly what I think it's intended to be. 
Except I'd tweak it to say that it's a command that you use to 
make a statement of fact (the program isn't doing anything).

> There is a distinct flavour to it. If I am wrong about an 'if' 
> statement, I will still be able tell how the program will 
> behave by inspecting the source code (if there is no other 
> source of UB), whereas the new assert semantics deny me this 
> possibility. I.e. my opinion is that "it's just like" is an 
> exaggeration, also because it is not me testing the 'if' 
> condition, but there it is obviously the program who is 
> commanded to do it.

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)

>
>> You'll get incorrect program behavior. Unlike those other
>> things, since it's verifiable, there exists some sort of 
>> configurations
>> where the program can be helpful to you by verifying your 
>> assertions.
>
> Type checking will be performed even in -release builds.
> I guess it is hard to reach consensus from here?

Well, there's a not-so-subtle difference between type checking 
and assertions. Whereas assertions could only be checked at 
runtime, failing to use typechecking in a statically compiled 
program means that you simply couldn't compile the program to 
begin with.

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