On 07/30/2014 11:42 PM, Walter Bright wrote:
> On 7/30/2014 2:34 PM, Timon Gehr wrote:
>> He understands that and notes that this contradicts the promise of @safe.
>
> No, it does not. @safe never promises that "all your asserts are correct".
>
> @safe's promise is one of memory safety,

Indeed it is.

> not a promise of program correctness.

There is some interplay.

void foo(size_t i,int[] a)@safe{
    assert(i<a.length);
    a[i] ='D'; // boom
}

Pass -release and the bounds check may be removed from the line annotated 'boom' based on the elided but assumed to be valid assertion, and your memory safety guarantee is out the window.

Unless one thinks incorrect programs shouldn't get any guarantees from @safe, this is a problem.

On 7/30/14, 3:06 PM, Timon Gehr wrote:
> On 07/30/2014 10:55 PM, Andrei Alexandrescu wrote:
>> On 7/30/14, 11:31 AM, Timon Gehr wrote:
>>> On 07/30/2014 07:56 PM, Andrei Alexandrescu wrote:
>>>> On 7/30/14, 9:31 AM, Timon Gehr wrote:
>>>>> 'lazy', which denotes pass by name instead of pass by need.
>>>>
>>>> It's not pass by name.
>>>> ...
>>>
>>> How so? Is it about failure to allocate a closure?
>>
>> void fun(lazy int a) { ... }
>> int x = 42;
>> fun(x + 2);
>>
>> "x + 2" doesn't have a name.
>> ...
>
> You might just have been fooled by the name of a concept.
>
> http://en.wikipedia.org/wiki/Evaluation_strategy#Call_by_name

Oh, yah. I'd forgotten. Mea culpa. Thanks!

>>>> Consider this: after considerable effort you are failing to explain
>>>> your
>>>> case for "assume" to the language creators.
>>>
>>> I think there was no such case (yet), only an unsuccessful attempt to
>>> clear up a misunderstanding based on terminology.
>>
>> My perception is you were arguing for a very subtle distinction,
>
> My perception is different. Why is this distinction so subtle?

Because it created a long thread in which there's little agreement.

>> one that would hardly deserve a language feature.
>> ...
>
> version(assert) is a slight generalisation of such a language feature
> and it is already there. I already noted how the distinction can be
> implemented approximately in current D, in fact I think this was my
> first action in this thread.
>
> version(assert) assert(...); // assert without effects on -release code
> generation.

Maybe this is a misundersanding. version(assert) does not mean "assert is considered here, else it's completely ignored". It means "assert will effect a run-time check".



Andrei

On 07/30/14 23:42, Walter Bright via Digitalmars-d wrote:
> On 7/30/2014 2:34 PM, Timon Gehr wrote:
>> He understands that and notes that this contradicts the promise of @safe.
> 
> No, it does not. @safe never promises that "all your asserts are correct".
> 
> @safe's promise is one of memory safety, not a promise of program correctness.

   void f(ubyte[] a) @safe { assert(a.length>99); a[88] = a[77]; }

artur

On 07/30/2014 11:39 PM, Walter Bright wrote:
> On 7/30/2014 2:21 PM, Timon Gehr wrote:
>> Because the compiler does not seem know that 'assert' never returns,
>> they shove
>> in an __assume after it.
>
> The critical bit of misunderstanding here is the C standard *requires*
> that assert be implemented as a macro,

There is no such misunderstanding. I know this.

> and that NDEBUG will totally disable it.

The example implementation based on NDEBUG there does not provide this, rather, NDEBUG leaves the optimizer hint in.

> Microsoft needed to add a builtin feature so that the
> correct assert semantics can be reliably obtained by the optimizer.
> ...

What makes the second implementation with both assert and __assume there 'correct'? Does the C standard specify undefined behaviour if the assert expression has side-effects?

> It's a mistake to infer from that that assert and assume are different.

I don't need to rely on the MSVC++ compiler to see this. (But the __assume they have can be used to pass hints to the optimizer even if it does not happen in the context of an assertion, which I think was bearophile's point.)

On 7/30/2014 3:20 PM, Artur Skawina via Digitalmars-d wrote:
> On 07/30/14 23:42, Walter Bright via Digitalmars-d wrote:
>> On 7/30/2014 2:34 PM, Timon Gehr wrote:
>>> He understands that and notes that this contradicts the promise of @safe.
>>
>> No, it does not. @safe never promises that "all your asserts are correct".
>>
>> @safe's promise is one of memory safety, not a promise of program correctness.
>
>     void f(ubyte[] a) @safe { assert(a.length>99); a[88] = a[77]; }

The compiler will insert array bounds checking for you.

On 7/30/2014 2:30 PM, Timon Gehr wrote:
> Did you read the article?
>
> http://en.wikipedia.org/wiki/Assertion_%28computing%29#Disabling_assertions
>
> '[...] disabling assertion checking can mean that a program that would have
> aborted will continue to run. This is sometimes preferable.'
>
> This is not what DMD does in -release where assertions are 'disabled'. It
> follows a diametrally opposite philosophy.

Not at all. The Wikipedia article does not argue that the program will continue in a valid state.

Walter Bright:

>>    void f(ubyte[] a) @safe { assert(a.length>99); a[88] = a[77]; }
>
> The compiler will insert array bounds checking for you.

But if your "assert" is the same as an assume(), then the optimizer should remove bounds checks (otherwise it's a lousy implementation of assume()) and leave no tests whatsoever inside the function f. So now you now have a safe function that is unsafe.

I think you are still missing the essential difference between assume and assert.

Bye,
bearophile

On Wednesday, 30 July 2014 at 22:30:59 UTC, Walter Bright wrote:
> On 7/30/2014 3:20 PM, Artur Skawina via Digitalmars-d wrote:
>>    void f(ubyte[] a) @safe { assert(a.length>99); a[88] = a[77]; }
>
> The compiler will insert array bounds checking for you.

Trying to understand what your position is: In release mode, but with bounds checking enabled, would the compiler
  a) be allowed to replace this with a RangeError or, say, ud2 or another halt()-type instruction?
  b) treat any call to f() as undefined behavior?

Cheers,
David

On 07/31/2014 12:17 AM, Andrei Alexandrescu wrote:
> On 7/30/14, 3:06 PM, Timon Gehr wrote:
>> On 07/30/2014 10:55 PM, Andrei Alexandrescu wrote:
>>> On 7/30/14, 11:31 AM, Timon Gehr wrote:
>>>> On 07/30/2014 07:56 PM, Andrei Alexandrescu wrote:
>>>>> ...
>>>>> case for "assume" to the language creators.
>>>>
>>>> I think there was no such case (yet), only an unsuccessful attempt to
>>>> clear up a misunderstanding based on terminology.
>>>
>>> My perception is you were arguing for a very subtle distinction,
>>
>> My perception is different. Why is this distinction so subtle?
>
> Because it created a long thread in which there's little agreement.
> ...

I've seen mostly agreement so far, but mostly not from you and Walter.

>>> one that would hardly deserve a language feature.
>>> ...
>>
>> version(assert) is a slight generalisation of such a language feature
>> and it is already there. I already noted how the distinction can be
>> implemented approximately in current D, in fact I think this was my
>> first action in this thread.
>>
>> version(assert) assert(...); // assert without effects on -release code
>> generation.
>
> Maybe this is a misundersanding.

I don't see how.

> version(assert) does not mean "assert
> is considered here, else it's completely ignored". It means "assert will
> effect a run-time check".
> ...

Indeed.

// original source:

void main(){
    int x=1;
    version(assert) assert(x==0);
    // ...
}


// after some lowering without the -release switch:

void main(){
    int x=1;
    assert(x==0); // version statement active,
    // check will be performed (and fail)
    // ...
}


// after some lowering with the -release switch:

void main(){
    int x=1;
    // version statement inactive, no check will be performed,
    // optimizer never sees the assertion
    // ...
}

I.e. no wrong assumptions are passed down to the optimizer under any circumstances if the assertion is guarded with version(assert).

On 07/31/14 00:31, Walter Bright via Digitalmars-d wrote:
> On 7/30/2014 3:20 PM, Artur Skawina via Digitalmars-d wrote:
>> On 07/30/14 23:42, Walter Bright via Digitalmars-d wrote:
>>> @safe's promise is one of memory safety, not a promise of program correctness.
>>
>>     void f(ubyte[] a) @safe { assert(a.length>99); a[88] = a[77]; }
> 
> The compiler will insert array bounds checking for you.

No, with the assert definition you're proposing, it won't. It would be allowed to optimize away the bounds check. And this is just one of many problems with the assert==assume approach.

artur