assert semantic change proposal

[via Digitalmars-d]

On Thursday, 7 August 2014 at 18:20:20 UTC, David Bregman wrote:
> On Thursday, 7 August 2014 at 18:02:08 UTC, Ola Fosheim Grøstad 
> wrote:
> I just gave you a concrete example of where assume(false) might 
> be useful for optimizing a switch statement.

But to me it sounds dangerous if it actually is reachable or if 
the compiler somehow think it is. So you should use halt() if it 
should be unreachable, and use unreachable() if you know 100% it 
holds. Encouraging assume(false) sounds like an aberration to me.

You need to provide proofs if you attempt using assume(X) and 
assert(false).

This is valid, but it is derived, not postulated:

assume(P)
while(false){

    assume(false)  // anything goes is acceptable over S here
    S…         // since it never happens…
    assert(P) // valid since the assumption is false

}
assert(P) // valid since the content is just a noop


When you postulate without proving you open a can of worms:

assume(P)
while(B){

    assume(false)  // woops! Should have been assume(B&&P)
    S…                  // ohoh we just stated anything goes in 
here…
    assert(P)          // invalid

}
assert(P)  // invalid since the loop invariant doesn't hold.



>> How do you define P1 and P2 to be different?
>
> I'm not sure how you'd define them to be the same. They're 
> different lines of code, for one thing.

I don't believe there "is" such a thing as lines of code. We are 
doing math. Everything just "is". We don't have code, we have 
mathematical dependencies/relations. P1 and P2 are propositions, 
so what are the content of those? The ones you use for your P1=>X 
and P2=>Y? You have to define newassume(P,X)===assume(P=>X). But 
what is P?

Anyway, you don't need those… You can use a regular 
assume(false), but not for indicating unreachable. You indicate 
that the postcondition does not have to hold. Otherwise you will 
run into trouble.

But if you think about while() as a short-hand that is expanded 
into pure math, then it makes sense. If you have while(true){} 
then the loop cannot generate new mathematical constants… Thus it 
cannot be a source for new unique propositions that let you 
discriminate between before and after entering the loop? Or?