On 08/06/14 10:28, eles via Digitalmars-d wrote:
> On Wednesday, 6 August 2014 at 07:29:02 UTC, Ola Fosheim Grøstad wrote:
>> On Wednesday, 6 August 2014 at 06:56:40 UTC, eles wrote:
> 
>> Not right:
>>
>> b = a+1
>> assume(b>C)
>>
>> implies
>>
>> assume(a+1>C)
>> b = a+1
> 
> b = a+1
> if(C<=b) exit(1);
> 
> implies
> 
> if(C<=a+1) exit(1);
> b = a+1
> 
> Is not the same? Still, one would allow the optimizer to exit before executing b=a+1 line (in the first version) based on that condition (considering no volatile variables).

It is *very* different. In the `exit` case this kind of transformation is only valid if that assignment has no externally observable effects. `assume` makes the transformation *unconditionally* valid, even when executing 'b=a+1' would affect the output of the program.

The compiler can /assume/ that the condition never fails. Hence, it does
not need to generate any code to check that the assumption is valid.
It does not need to emit any code for any path that would only be taken
if the condition would be false. If that ever happens the CPU can start
executing any random instructions. That's ok, since you explicitly told
the compiler that this situation will never occur. Hence, it can also
skip generating any code for any path that unconditionally leads to a
failing `assume` directive. Because it is all dead code that will never
be executed, as long as all `assume` conditions are true.

artur

On Wednesday, 6 August 2014 at 12:41:16 UTC, Artur Skawina via Digitalmars-d wrote:
> The compiler can /assume/ that the condition never fails. Hence, it does
> not need to generate any code to check that the assumption is valid.

Exactly, worse example using a coroutine:

«
label:
…
while(running) { // forevah!
   … yield …
}
…
assume(anything local not assigned below label) // reachable, but never executed
»

is equivalent to:

«
assume(anything local not assigned below label) // optimize based on this
label:
…
while(running) {
   … yield …
}
»

Woops?

On Wednesday, 6 August 2014 at 13:31:54 UTC, Ola Fosheim Grøstad wrote:
> On Wednesday, 6 August 2014 at 12:41:16 UTC, Artur Skawina via Digitalmars-d wrote:
>> The compiler can /assume/ that the condition never fails. Hence, it does
>> not need to generate any code to check that the assumption is valid.
>
> Exactly, worse example using a coroutine:
>
> «
> label:
> …
> while(running) { // forevah!
>    … yield …
> }
> …
> assume(anything local not assigned below label) // reachable, but never executed
> »
>
> is equivalent to:
>
> «
> assume(anything local not assigned below label) // optimize based on this
> label:
> …
> while(running) {
>    … yield …
> }
> »
>
> Woops?

But even if there is no explicit assert()/assume() given by the developer, I guess the optimizer is free to insert assumes that are provably correct, e.g.

  while(running) {
    ...don't assign to running, don't break...
  }

is equivalent to

  while(running) {
    ...don't assign to running, don't break...
  }
  assume(!running);

is equivalent to

  assume(!running);
  while(running) {
    ...don't assign to running, don't break...
  }

is equivalent to

  assume(!running);


So I take the compiler is allowed to throw away code without any asserts already ?

On Wednesday, 6 August 2014 at 15:02:10 UTC, Matthias Bentrup wrote:
> So I take the compiler is allowed to throw away code without any asserts already ?

Yes it can, but only in the cases where it can prove it is the same.

The main difference is that assume does not need to be proved, it is stated to always be true so no proof needed. Some have said that the compiler can still try to prove what it can and issue warnings if it is provable untrue, but it would actually be a little silly on the part of the compiler to waist it's time trying to disprove things it "knows" are true. If it "knows" it is true then why even bother checking?

On Wednesday, 6 August 2014 at 15:02:10 UTC, Matthias Bentrup wrote:
> is equivalent to
>
>   while(running) {
>     ...don't assign to running, don't break...
>   }
>   assume(!running);

You have to prove termination to get there? Plain Hoare logic cannot deal with non-terminating loops. Otherwise you risk proving any theorem below the loop to hold?

But I was talking about explicit assumptions made by the programmer, who does not know the rules… It was obviously wrong to assume anything to hold if the loop never terminates.

The rule for proving loop termination is quite involved where you basically prove that every time  you move through the loop you get something "less" than you had before (ensured by t and  D). This is no fun, and a good reason to hate reasoning about correctness:

a < b: is a well-founded ordering on the set D

if this holds:

[P ∧ B ∧ t ∈ D ∧ t = z]   S   [P ∧ t ∈ D ∧ t < z ]

then this holds:

[P ∧ t ∈ D]   while B do S done   [¬B ∧ P ∧ t ∈ D]

I think… or maybe not. Who can tell from just glancing at it?

On Wednesday, 6 August 2014 at 15:29:13 UTC, Ola Fosheim Grøstad wrote:
> On Wednesday, 6 August 2014 at 15:02:10 UTC, Matthias Bentrup wrote:
>> is equivalent to
>>
>>  while(running) {
>>    ...don't assign to running, don't break...
>>  }
>>  assume(!running);
>
> You have to prove termination to get there? Plain Hoare logic cannot deal with non-terminating loops. Otherwise you risk proving any theorem below the loop to hold?

This is an assume, not an assert. The user tells the compiler that `running` is false after the loop, it can thus conclude that the loop will never run. So there is no non-terminating loop in this case.

On 08/06/14 17:02, Matthias Bentrup via Digitalmars-d wrote:
> But even if there is no explicit assert()/assume() given by the developer, I guess the optimizer is free to insert assumes that are provably correct, e.g.
> 
>   while(running) {
>     ...don't assign to running, don't break...
>   }
> 
> is equivalent to
> 
>   while(running) {
>     ...don't assign to running, don't break...
>   }
>   assume(!running);

In the "running==true" case that 'assume' will never be reached...

> is equivalent to
> 
>   assume(!running);
>   while(running) {
>     ...don't assign to running, don't break...
>   }

... so, no, this transformation is not a valid one.

> So I take the compiler is allowed to throw away code without any asserts already ?

It can do whatever it wants, as long as the observable behavior does not change. `Assume` removes that restriction as soon as a failing assert is reached.

artur

On Wednesday, 6 August 2014 at 08:25:38 UTC, Walter Bright wrote:

Thank you for the well thought out response.

> I responded to the equivalent design proposal several times already, with detailed answers. This one is shorter, but the essential aspects are there. I know those negative aspects came across because they are addressed with your counter:

I was not trying to attack you, but rather inform you. I think that is all I want to say on the subject so I am going to stop talking about it.

> 1. it's long with an unappealing hackish look

I find this a positive, the proposed assert has quite dangerous implications, having a slightly "hackish" look will serve to discourage using it when it is not obviously needed.

> 2. it follows in the C++ tradition of the best practice being the long ugly way, and the deprecated practice is the straightforward way (see arrays in C++)

That is implying that the best practice is your version of assert. As it can introduce undefined behavior, I find it hard to believe.

> 3. users will be faced with two kinds of asserts, with a subtle difference that is hard to explain, hard to remember which is which, and will most likely use inappropriately

This is why I think it would be best added as an annotation on assert. People who don't care enough to look up what the extra annotation does will just use assert by itself and have no risk of undefined behavior and it will behave as expected(similar to how it behaves in other languages).


> 4. everyone who wants faster assert optimizations will have to rewrite their (possibly extensive) use of asserts that we'd told them was best practice. I know I'd be unhappy about having to do such to my D code.

This is a fare point but it would happen the same either way. If some one used assert expecting it to act like the C assert and found out it did not any more, they would be forced to go through though there code and change all the asserts. As this is a change, I am inclined to say we should favor the old version and not force users of the old version to update.

> This is not about my feelings, other than my desire to find the best design based on a number of tradeoffs.

I was just trying to say that it is a possibility that should not be forgotten, I think I may have said it in a harsher way than I meant to, I apologize. The annotated assert was my attempt at a possible compromise.

On Wednesday, 6 August 2014 at 15:36:52 UTC, Marc Schütz wrote:
> This is an assume, not an assert.

Not sure what you mean. An assume is an assert proven (or defined) to hold. It can be a proven theorem which has been given the status of an axiom. It is known to keep the algebraic system sound. If you claim that something unsound is proven then all bets are off everywhere?

I am quite confident that assume(false) anywhere in your program is basically stating that the program is unsound (true==false) and should not be compiled and run at all. If true==false anywhere in your program then it surely holds everywhere in your program?

The only reason c-style assert(false) "works", is because you delay the verification until the last moment, at which point the system says "woopsie", gotta terminate this because this program should never have compiled in the first place.

Sounds consistent to me?

On Wednesday, 6 August 2014 at 08:25:38 UTC, Walter Bright wrote:
> On 8/5/2014 11:28 PM, Tofu Ninja wrote:
>> Please stop responding in such a dismissive way, I think it is
>> already pretty obvious that some are getting frustrated by these
>> threads. Responding in a dismissive way makes it seem like you
>> don't take the arguments seriously.
>
> I responded to the equivalent design proposal several times already, with detailed answers. This one is shorter, but the essential aspects are there. I know those negative aspects came across because they are addressed with your counter:

I don't think I've seen your arguments against adding assume(), last time this was discussed you were still claiming that there was no difference between the two, so we couldn't even get to discussing it!

>
> > How about something like
> > @expected assert(x > 2); or @assumed assert(x > 2);
> > It wouldn't introduce a new keyword, but still introduces the
> expected/assumed semantics.
>
> The riposte:
>
> 1. it's long with an unappealing hackish look
> 2. it follows in the C++ tradition of the best practice being the long ugly way, and the deprecated practice is the straightforward way (see arrays in C++)
> 3. users will be faced with two kinds of asserts, with a subtle difference that is hard to explain, hard to remember which is which, and will most likely use inappropriately
> 4. everyone who wants faster assert optimizations will have to rewrite their (possibly extensive) use of asserts that we'd told them was best practice. I know I'd be unhappy about having to do such to my D code.
>

Nice, this is progress. You're giving us some actual reasoning! :)

Is this the full list of your reasons or just a subset?

1, 2:
Those don't apply to assume() without the annotations right? I agree that's hacky looking with annotations.

3:
If the separation is not made official, a lot of people will end up having to roll their own, potentially with all kinds of names. This is much more fragmenting than just having official assert and assume. myAssert, debugCheck, smurfAssert, etc. ugh.

As for the difference being subtle, hard to remember, understand, or explain: This totally supports my argument. If people don't even understand the subtlety, there's no way they are ready to be inserting undefined behavior everywhere in their code. assume (or your assert) is a dangerous power tool, joe coder probably shouldn't be using it at all. Yet you want it used everywhere by default?

4:
This is a valid argument. The flip side is that everyone else has to invent their own function and rewrite their code with it, unless they have 100% faith their code is not buggy, or don't care about undefined behavior (or don't know they care about it until they get bitten by it later). Or if they go for the quick fix by disabling -release, then you just pessimized their code instead of optimized it. Plus what about people who miss the change, or unmaintained code?

Isn't the default way of doing things to err on the side of not breaking people's code? Why is this time different? I know you hate more switches (for good reason), but this seems like a good case for -Oassert or -Ounsafe, for the elite few people whose code is actually suitable for such dangerous transformation.


I would like to note some additional benefits of separating the two concepts and hopefully get your thoughts on these. Some of these are repeating from previous posts.

-assert(0) is defined as a special case, so it can't express unreachability. This makes it less powerful for optimizing than it should be. assume(0) does not have this problem. e.g. switch(){ /* ... */ default: assume(0); }

-the proposed assert is not @safe, which creates complications since the current assert is. assume() does not have this problem, as it can be defined as @system from the start.

-with the functions separate, it can be made clear that assume() is a dangerous tool that should be used sparingly. It will mean that code is more searchable and easier to audit - if there is a heisenbug, try a search for @trusted and assume() constructs.

-retain C compatibility, which is supposed to be a goal of D.