assert semantic change proposal

[via Digitalmars-d]

On Thursday, 7 August 2014 at 17:38:22 UTC, David Bregman wrote:
> Using my definition of assume, the axiom declared is P=>x. If P 
> is false, then the axiom declared is false => x, which is true 
> for any x.

I don't see how this will work out. If it is truly unreachable 
then you don't need any assume, because then you can assert 
anything. Therefore you shouldn't.

valid:

assume(true)
while(true){}
assert(angels_love_pixiedust) //proven true now…

But there are alternatives to HL that I don't know much about. 
You might want to look at "Matching Logic Reachability". Looks 
complicated:

http://fsl.cs.illinois.edu/pubs/rosu-stefanescu-2012-fm.pdf


> Ok, is it clear now? If not, which parts are not clear?

It doesn't make any sense to me since I don't see how you would 
discriminate between your Ps.

{P1}
while(true) skip; endwhile
{P2}

How do you define P1 and P2 to be different?