July 30, 2014
"Walter Bright"  wrote in message news:lrbes7$9gs$1@digitalmars.com...

> enforce is NOT for checking program logic bugs, it is for checking for possible environmental failures, like writing to a read-only file.
>
> If you want an assert to be there even in release mode,
>
>      assert(exp) => exp || assert(0)

As I said earlier, this is valid by what dmd currently implements, but not according to the spec.  The spec does not guarantee assert(0) checks will always be emitted. 

July 30, 2014
To release software is to assume that it is correct.
July 30, 2014
On 07/30/2014 08:39 PM, Daniel Murphy wrote:
> "Wyatt"  wrote in message news:duoyilszsehayiffprls@forum.dlang.org...
>
>> Something (possibly the thing where "For fastest executables, compile
>> with the -O -release -inline -boundscheck=off" is standard advice to
>> anyone asking about performance) tells me this point needs to be made
>> MUCH more clear wherever possible or the ghost of Scott Meyers will
>> haunt us all. But that it's even a problem tells me we're facing a
>> pattern of human error.  Is there no good way to eliminate it?
>
> Well, that will give you the fastest possible code.  But there is no
> guarantee that small mistakes won't blow up in your face.  It could be
> hidden behind another compiler switch (-release is really a terrible
> name, maybe -livefastdieyoung ?  -noparachute ?
> -drinkthemysteyliquidreadthelabellater ?) but chances are it will be
> abused no matter what.

On 07/30/2014 08:42 PM, Daniel Murphy wrote:> "Dicebot"  wrote in message news:kvxcdcbgjwyydrjgbijg@forum.dlang.org...
>> At the same time "release" is rather encouraging flag to use, it is
>> not like it is called "-iamreadyfortheconsequences".
>
> -idontcareificrashsolongasicrashfast

Maybe we should rename all D keywords in this distinctive style.

July 30, 2014
On 07/30/2014 08:46 PM, H. S. Teoh via Digitalmars-d wrote:
> I can't think of a real-life scenario where you'd want to distinguish
> between the two kinds of optimizations in (2).

That was never up to debate and that distinction is indeed rather pointless.
July 30, 2014
On Wednesday, 30 July 2014 at 18:25:43 UTC, H. S. Teoh via Digitalmars-d wrote:
> If you want the check to always be there, use enforce, not assert.

Doesn't help:

    module a;
    void bar(int x) {
        assert(x > 0);
        writeln("x = ", x);
    }
    // --------
    module b;
    import a;
    void foo(int x) {
        enforce(x > 0);
        bar(x);
    }

If `assert` is treated like `assume` (under Ola's definitions), then `enforce` can be optimized away.
July 30, 2014
On Wed, Jul 30, 2014 at 07:09:41PM +0000, via Digitalmars-d wrote:
> On Wednesday, 30 July 2014 at 18:25:43 UTC, H. S. Teoh via Digitalmars-d wrote:
> >If you want the check to always be there, use enforce, not assert.
> 
> Doesn't help:
> 
>     module a;
>     void bar(int x) {
>         assert(x > 0);
>         writeln("x = ", x);
>     }
>     // --------
>     module b;
>     import a;
>     void foo(int x) {
>         enforce(x > 0);
>         bar(x);
>     }
> 
> If `assert` is treated like `assume` (under Ola's definitions), then
> `enforce` can be optimized away.

Wait, what? I thought the whole point of enforce is that it will *not* be removed by the compiler, no matter what?


T

-- 
Debugging is twice as hard as writing the code in the first place. Therefore, if you write the code as cleverly as possible, you are, by definition, not smart enough to debug it. -- Brian W. Kernighan
July 30, 2014
On Wednesday, 30 July 2014 at 18:48:21 UTC, H. S. Teoh via Digitalmars-d wrote:
> 1) When compiling in non-release mode:
> 	assert(...) means "I believe condition X holds, if it doesn't I
> 		screwed up big time, my program should abort"

Assert(X) means, the specification requires theorem X to be proved by all implicit or explicit axioms/assumptions made prior to this either implicitly or explicitly.

> 	assume(...) means as "I believe condition X holds, if it doesn't
> 		I screwed up big time, my program should abort"

Assume(X) means, the specification specifies (axiom) X (to hold).

> 2) When compiling in release/optimized mode:
> 	assert(...) means "Trust me, I've made sure condition X holds,
> 		please optimize my code by not bothering to check
> 		condition X again"

No. Assert(X) does not change any meaning. You just turned off program verification. Assumes and asserts are annotations.

> 	assume(...) means "Trust me, I've made sure condition X holds,
> 		please optimize my code by making use of condition X"

Assume(X) means that the specification defines X to hold at this point.

> in (2), but I don't see the incompatibility. In both cases under (2) we
> are *assuming*, without proof or check, that X holds, and based on that
> we are making some optimizations of the generated code.

Not really. Most of the assumes are implicit in the code. What you specify with assume are just additional axioms required by the specification in order to prove the assertions. (e.g. the ones not embedded implicitly in the code).

> I can't think of a real-life scenario where you'd want to distinguish
> between the two kinds of optimizations in (2).

The difference is that "assume(X)" (or require) are the specified preconditions. It does not make the program incorrect per definition. However you don't want your program littered with preconditions.

So yes, you CAN optimize based on assume() since those are restrictions the environment put on the input. But you only have a few of those.
July 30, 2014
On 07/30/2014 09:16 PM, H. S. Teoh via Digitalmars-d wrote:
> On Wed, Jul 30, 2014 at 07:09:41PM +0000, via Digitalmars-d wrote:
>> On Wednesday, 30 July 2014 at 18:25:43 UTC, H. S. Teoh via Digitalmars-d
>> wrote:
>>> If you want the check to always be there, use enforce, not assert.
>>
>> Doesn't help:
>>
>>      module a;
>>      void bar(int x) {
>>          assert(x > 0);
>>          writeln("x = ", x);
>>      }
>>      // --------
>>      module b;
>>      import a;
>>      void foo(int x) {
>>          enforce(x > 0);
>>          bar(x);
>>      }
>>
>> If `assert` is treated like `assume` (under Ola's definitions), then
>> `enforce` can be optimized away.
>
> Wait, what? I thought the whole point of enforce is that it will *not*
> be removed by the compiler, no matter what?
>
>
> T
>

That's approximately the crux of the matter, yes. :-)
July 30, 2014
On Wednesday, 30 July 2014 at 18:13:07 UTC, Ary Borenszweig wrote:
> I tried the program in debug mode in thousands of ways and apparently no assert triggers. So I'll just compile in release mode, release it and let anyone find bugs in it and allow to bypass any security or safety I put in my program with those "assert" statmenets, that would probably just take 1 nanosecond to execute anyway.
>
> Sounds really nice.
>
> (sorry for the sarcasm, removing assert is wrong to me)

Use enforce...
July 30, 2014
On Wednesday, 30 July 2014 at 14:36:30 UTC, Ary Borenszweig wrote:
> Could you show an example that's a bit more complex and useful? I'm with Walter that I don't see any difference between assert and assume.

assume provide additional axioms to the ones implicit in the program.
assert provide theorems to be proven.

assume provide claims that already are proven (or just defined as a requirement imposed on the environment).

For instance after a system call, you might have a specification that states exactly what you can assume after it returns. That specification you can specify as assume() and you can optimize on those, safely.

assert() you cannot optimize on safely. Those are theorems that are yet to be proven.