assert semantic change proposal

[via Digitalmars-d]

On Wednesday, 6 August 2014 at 21:33:35 UTC, Timon Gehr wrote:
> On 08/06/2014 11:18 PM, Matthias Bentrup wrote:
>>
>> Ah, I had a different understanding of assume, i.e. placing an
>> assume(A) at some point in code adds not the axiom A, but 
>> rather
>> the axiom "control flow reaches this spot => A".
>
> (Your understanding is the conventional one.)

Not right.

You need to take into account that assume() provides a 
mathematical definition, it isn't an imperative. That would make 
no sense. So there is no control flow, only mathematical 
dependencies.

You only deal with constants. "Variables" are just a tool for 
automatic labeling of constants. You would not be able to use 
logic otherwise.

"Control flow" is embedded in the dependencies and relationships 
between the constants.

j=0
for(i=0; i<3;++i){j+=i}

Is just a short-hand for:

j0 = 0
i0 = 0
j1 = j0 + i0
i1 = 1
j2 = j1 + i1
i2 = 2
j3 = j2 + i2

If you map this out as a graph you get the dependencies 
(mirroring "control flow").

Hoare-logic provide means to reason about the short-hand notation 
and make transformations on it.

What is unconventional about this?