assume, assert, enforce, @safe

[Timon Gehr via Digitalmars-d]

On 07/31/2014 08:58 PM, Walter Bright wrote:
> On 7/31/2014 4:28 AM, David Bregman wrote:
>> Sigh. Of course you can assume the condition after a runtime check has
>> been
>> inserted. You just showed that
>>
>> assert(x); assume(x);
>>
>> is semantically equivalent to
>> assert(x);
>>
>> as long as the runtime check is not elided. (no -release)
>
> No. I showed that you cannot have an assert without the assume.

No you did not. However:

* You showed that an additional 'assume' would not have any effect if 
the check is never elided.

* You showed that the state of knowledge about the program state of the 
optimizer are the same after processing a halting runtime check and 
after processing an 'assume'.

I don't think anybody is contesting that. Now try to zoom your focus out 
a little, and think about _what if_ the assertion and the assumption are 
actually wrong? Why does it make sense to conflate them in this case?

> That makes them equivalent that direction.
>
> For the other direction, adding in a runtime check for an assume is
> going to be expected of an implementation.

Yes if 'assert' does what 'assert' does now, and if 'assume' does what 
'assert' does now, then 'assert' and 'assume' do the same. I agree with 
that, but the premise is unrelated to this discussion. You are moving 
the goal posts.

> And, in fact, since the
> runtime check won't change the semantics if the assume is correct, they
> are equivalent.
> ...

"If the 'assume'/'assert' are correct" is not a sound assumption to 
make. You are not the compiler, you are the programmer. We are 
discussing _about_ programs, not _within_ programs.

> I.e. for practical purposes, they are the same thing.

All assertions being correct is not a given 'for practical purposes'. 
You are arguing in the context of a theoretical ideal and this context 
alone.