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)
