assert semantic change proposal

[David Bregman via Digitalmars-d]

On Thursday, 7 August 2014 at 19:41:44 UTC, Ola Fosheim Grøstad 
wrote:
> 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.

It is dangerous, and shouldn't be used lightly. That's what 
started this whole thread.

> So you should use halt() if it should be unreachable,

Not if your goal is to completely optimize away any unreachable 
code.

> and use unreachable() if you know 100% it holds.

This is just another name for the same thing, it isn't any more 
or less dangerous.

> Encouraging assume(false) sounds like an aberration to me.

If you accept my definition of assume there is no problem with 
it, it just means unreachable. I showed how this follows 
naturally from my definition.

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

There is no mechanism for providing proofs or checking proofs in 
D.

>>> 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.

Well, any correct mathematical formalism of the code must 
preserve its semantics, so it doesn't really matter which one we 
talk about.

Different lines (or basic blocks, I guess is the right term here) 
can have different reachability, so you could just give each one 
its own P.

> P1 and P2 are propositions, so what are the content of those? 
> The ones you use for your P1=>X and P2=>Y?

This is just an implementation detail of the compiler. Probably 
each basic block has its own P, which is conservatively 
approximated with some data flow analysis. (Disclaimer: I am not 
a compiler expert)

> 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?

Sorry, I don't understand much of this.

Anyways, I don't have much more time to keep justifying my 
definition of assume. If you still don't like mine, maybe you can 
give your definition of assume, and demonstrate how that 
definition is more useful in the context of D.