checkedint call removal

[via Digitalmars-d]

On Wednesday, 30 July 2014 at 12:11:31 UTC, Daniel Murphy wrote:
> So you'll be happy if we call them D-style assertions?

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.

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.

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.