checkedint call removal

[via Digitalmars-d]

On Friday, 1 August 2014 at 11:53:28 UTC, Don wrote:
> The arguments presented by Ola et al mostly seem to be 
> arguments against the use of the -release switch. Because it is

No, I think I do understand where Walter is coming from now. I 
remember some of the incomprehensible lectures I attended as a 
student where the entire blackboard was filled with quantors this 
and that.

I have spent hours every day the past few days thinking about how 
to explain it efficiently. I think D will benefit greatly if 
Walter dig into some of the theories on formal program 
verification, but everybody has to take rounds of the heuristic 
cycle to truly get down to it. So it is good that he does not 
accept it without an argument.

It is just not a topic where you can read one article and you 
will shout "eureka!". So I don't think it is a good idea to just 
say "oh it is just about -release". It is basically about finding 
common ground where program verification gets the best treatment 
possible and in a manner that is consistent with how users with a 
CS background perceive correctness.


I hope this gets us closer to common ground:


Let's assume with have a simple program like this:

int program(immutable string input){
	int r = input.length + input.length;
	assert(r == 2* input.length);
	return r;
}


Then execute it:
interpreter> run program "hi"


Then we have the following situation iff it completes 
successfully:

PROVEN:
if input=='hi' then input.length + input.length == 2* input.length

EQUIVALENT TO:

(input != 'hi') || (input.length + input.length == 2* 
input.length)


NOT PROVEN YET:
input.length + input.length == 2* input.length for all input != 
'hi'


That basically means that a formal assert(x) and a runtime check 
has the following relationship:

runtime_assert(x) is the same as formal_prove( input!=ACTUALINPUT 
|| x )

formal_assert(x) is the same as formal_prove(x)