checkedint call removal

[Daniel Murphy via Digitalmars-d]

"Ola Fosheim Grøstad" " wrote in message 
news:umhhokwldfouodjhvooh at forum.dlang.org...

> Program verification has been at the core of CS for over 40 years. This is 
> bachelor grade stuff. If you keep inventing your own semantics for 
> well-established terminology then nobody will take D seriously.

It sure seems easy to make D not be taken seriously.  Every day somebody's 
making this claim about something.

> For instance, if assert(false) is proven reachable then it means either:
>
> 1. the specification is inconsistent/contradictory (thus wrong)
> 2. the program has been proved incorrect
>
> The compiler should then refuse to generate code. If it is not proven 
> reachable then emitting HALT might be ok.

You say this as if it's a law of physics.  One of the great things about 
working on D is that we get to assign the semantics that we decide are most 
useful, and don't have to follow what other people have done.

A good example is D's purity.  It doesn't match traditional definitions of 
purity, but it's useful.  I'm sure that's another reason not to take D 
seriously.

> Basically D ought to allow a verifier to work on a D program, then only 
> emit runtime checks for asserts it cannot handle. And also allow them to 
> trigger as early as possible.

You're just saying it should work the way you think it should work.  The 
fact that other people have defined it that way before does not outweigh the 
value of defining assert the way I've described IMO.  I don't think the 
safety concerns are warranted either, due to the existing optimizer 
precedent.

Any verifier for D would have to understand the semantics of D's assert.  If 
the verifier assumes asserts are always replaced with a runtime check, then 
it will be fine as long as you don't compile with -release.