On 7/30/14, 7:55 AM, Tofu Ninja wrote:
> On Wednesday, 30 July 2014 at 14:51:34 UTC, Andrei Alexandrescu wrote:
>> Also, it's unclear to me what the optimizer would be supposed to do if
>> an assumption turns out to be false.
>
> Bad... bad... things...

So then I see nothing that assume can do that assert can't. -- Andrei

On 7/30/14, 11:44 AM, Daniel Murphy wrote:
> "Ary Borenszweig"  wrote in message news:lravtd$2siq$1@digitalmars.com...
>
>> Now, if you compile in release mode, according to Walter, all the
>> "asserts" are gone (which, as a side note, is something I don't like:
>> in every case it should throw an AssertError). So the question is: can
>> the compiler still replace that writeln call? It should, but since
>> there's nothing there preventing x + y to be different than 3 (the
>> assertion is gone), the compiler can't replace it anymore.
>
> That's the whole point - the compiler theoretically can optimize as if
> the assert is checked.
>
> (This example uses assert(0) because this behaviour is actually in the
> spec)
>
> if (x != 3) assert(0);
> if (x == 3) deleteAllMyFiles();
>
> The compiler is allowed to treat assert(0) as unreachable - and if it's
> unreachable then it must be impossible for x to be != 3.
>
> So it becomes:
>
> deleteAllMyFiles();
>
> He's asking for assert to mean 'check this condition' and assume to mean
> 'optimize as if this is a mathematical identity'.

And how is that different if instead of:

if (x != 3) assert(0);

you write:

assume(x != 3);

?

"Andrei Alexandrescu"  wrote in message news:lrb1ru$30ag$1@digitalmars.com...

> It's better when you need an expression. -- Andrei

Nooooo!  That's the kind of thinking that leads to using the comma operator!!!! 

"Ary Borenszweig"  wrote in message news:lrb21p$30lf$1@digitalmars.com...

> > He's asking for assert to mean 'check this condition' and assume to mean
> > 'optimize as if this is a mathematical identity'.
>
> And how is that different if instead of:
>
> if (x != 3) assert(0);
>
> you write:
>
> assume(x != 3);

Because if assert only means 'check this condition' then the optimizer can't optimize based on the assumption that it's true. 

"Andrei Alexandrescu"  wrote in message news:lrb20i$30jl$1@digitalmars.com...

> So then I see nothing that assume can do that assert can't. -- Andrei

assume can avoid confusing people that think D's assert means something it doesn't. 

On 07/30/2014 09:22 AM, "Ola Fosheim =?UTF-8?B?R3LDuHN0YWQi?= <ola.fosheim.grostad+dlang@gmail.com>" wrote:
> On Tuesday, 29 July 2014 at 22:07:42 UTC, Timon Gehr wrote:
>> On 07/29/2014 11:08 PM, "Ola Fosheim =?UTF-8?B?R3LDuHN0YWQi?=
>> <ola.fosheim.grostad+dlang@gmail.com>" wrote:
>>> The best you can hope to have is partial correctness. Even with a system
>>> for formal verification.
>>
>> Well, why would this be true?
>
> Because there is no way you can prove say OpenGL drivers to be correct.
> They are a black box provided by the execution environment.

I see. (Though I secretly still dare to hope for verified OpenGL drivers, or something analogous: it is not completely out of reach theoretically; the machine can be given a quite precise formal specification.)

Note that 'partial correctness' usually means that the program runs correctly conditional on its termination, hence my confusion.

On Wed, Jul 30, 2014 at 08:12:20AM -0700, Andrei Alexandrescu via Digitalmars-d wrote:
> On 7/30/14, 7:55 AM, Tofu Ninja wrote:
> >On Wednesday, 30 July 2014 at 14:51:34 UTC, Andrei Alexandrescu wrote:
> >>Also, it's unclear to me what the optimizer would be supposed to do if an assumption turns out to be false.
> >
> >Bad... bad... things...
> 
> So then I see nothing that assume can do that assert can't. -- Andrei

Yeah, I think this hair-splitting between assume and assert is ... pure hair-splitting. I don't know where people got the idea that assert means "check this condition" as opposed to "assume this condition is true and generate code accordingly". My understanding of it is that it's telling the compiler (and whoever reads the code), that at that given juncture in the code, the programmer has assured that a certain condition holds, and that the following code was written with that assumption in mind.

The fact that assert will fail at runtime is a secondary artifact to help catch logic errors where the programmer's assumptions somehow got broken. IOW, it's something extra the compiler throws in, in order to help with debugging; it is strictly speaking not part of the program logic. The compiler is merely saying, "OK the programmer says condition X must hold at this point. But just in case he made a mistake, I'll throw in a check that will fail at runtime so that if he *did* make a mistake, the program won't blunder onwards blindly and do stupid things because it made a wrong assumption." It's not *that* far a stretch for the compiler to also say, "OK the programmer says condition X must hold at this point. I trust him, so I'm going to optimize the following code accordingly."

To me, it totally makes sense for the compiler to apply the former approach when compiling in non-release mode (which is by definition when the programmer is developing and testing the program, and would appreciate the extra help in assumptions being checked), and the latter approach when compiling in release/optimizing mode (which is by definition where the programmer wants to take maximum advantage of any optimizations the compiler can do -- so optimizations stemming from assert's are fair game as the source of possible code simplifications).


T

-- 
Written on the window of a clothing store: No shirt, no shoes, no service.

On Wednesday, 30 July 2014 at 14:55:48 UTC, Tofu Ninja wrote:
> On Wednesday, 30 July 2014 at 14:51:34 UTC, Andrei Alexandrescu wrote:
>> Also, it's unclear to me what the optimizer would be supposed to do if an assumption turns out to be false.
>
> Bad... bad... things...

That is the main argument(not saying I support it) for separating assert and assume, assert acts like assume in -release, and if an assume is false then bad things can happen.

Question?
If an if condition throws or returns in its body is it ok for the optimizer to 'assume' that the condition is false after and make optimizations for it? If so then every one complaining that assert gets removed in -release should really just be using enforce.

after all en enforce is simply

if(!(cond))  // can be removed if cond is provably true, same as assert could be removed
     throw ...;
// Can safely assume cond is true from this point on up until the first catch...

The possibility for the optimizer to make the same optimizations for assert can be done for enforce, the only difference is that it does not get removed in -release....

"Timon Gehr"  wrote in message news:lrb2o9$314b$1@digitalmars.com...

> > Because there is no way you can prove say OpenGL drivers to be correct.
> > They are a black box provided by the execution environment.
>
> I see. (Though I secretly still dare to hope for verified OpenGL drivers, or something analogous: it is not completely out of reach theoretically; the machine can be given a quite precise formal specification.)

But even if the drivers are verified, the hardware might be buggy!  And if the hardware's verified, the power source might be unstable! 

On Wednesday, 30 July 2014 at 15:24:57 UTC, Timon Gehr wrote:
> I see. (Though I secretly still dare to hope for verified OpenGL drivers, or something analogous: it is not completely out of reach theoretically; the machine can be given a quite precise formal specification.)

There is literally no chance in hell for a verified opengl driver. The number of permutations on the state alone is astronomical and un-testable. Its made even worse by the fact that the hardware changes every year or so.

Sources: I am doing an internship at nvidia right now :P