checkedint call removal

[via Digitalmars-d]

On Wednesday, 30 July 2014 at 13:14:11 UTC, Daniel Murphy wrote:
>> 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.

It follows the law of logic:

http://en.wikipedia.org/wiki/Hoare_logic
http://en.wikipedia.org/wiki/Propositional_calculus

> Any verifier for D would have to understand the semantics of 
> D's assert.

If D gets this it will be a general verifier adapted to D. That 
follows the rules of established sound logic developed over the 
past 2300 years.

All asserts should be established as either true or unknown. 
Assert(false) is weird. It is basically saying that true==false 
and asks you to prove that over a statement/loop that may or may 
not terminate.

http://coq.inria.fr/distrib/8.2/contribs/HoareTut.exgcd.html

«Basic Hoare logic is not well-suited for reasoning about 
non-terminating programs. In total correctness, postconditions of 
non-terminating programs are not provable. In partial 
correctness, a non-terminating program satisfies any 
(unsatisfiable) postcondition.»