On 8/1/2014 1:43 AM, bearophile wrote:
> John Colvin:
>
>> This is enough to convince me.
>
> Please don't feed Walter.

I don't care if you make such remarks about me, but I do care about the level of discourse in the forum sinking to such levels. Please refrain from such.

On Friday, 1 August 2014 at 03:58:22 UTC, Walter Bright wrote:

> If you look at the Wikipedia article,
>
>   http://en.wikipedia.org/wiki/Assertion_(software_development)
>
> you'll see a more high level view of what assert is all about, rather than a worm's eye view the C standard takes. (It even uses C for its examples.) Up until this thread, I've never encountered someone who thought differently about it.

I just read that and it matches my idea of what asserts are all about. But nowhere could I see any mention of asserts being a promise to the compiler that it could then reason from. The article mentions reasoning but I read that as human reasoning. This sentence:

"The use of assertions helps the programmer design, develop, and reason about a program."

To me sums it up. I dislike the idea of the compiler reasoning from the assertions because, to me, it hinders the programmer's ability to develop a program.

That said: From what Jonathan has said, it sound like this argument could be recast as one about what the "-release" option means. If it's avoidable without losing other optimizations, I don't feel hindered in any way, and this is just a question about user surprise, naming and documentation.

On Friday, 1 August 2014 at 09:02:36 UTC, Walter Bright wrote:
> On 7/31/2014 11:24 PM, "Ola Fosheim Grøstad"
>> An assert does not say that the predicate is always true.
>
> Yes, it does. From Meyers' comprehensive tome on the topic "Object-Oriented Software Construction" (1997) where he writes:
>
> "A run-time assertion violation is the manifestation of a bug in the software."

No. Implication is not the same as equivalence.

An assert does not take a predicate. It takes a proposition that is to be turned into a proven theorem.

bool test(bool x) {return x || !x} // predicate

test(x) for all x in {true,false} // proposition

assert(test(x) for all x in {true,false}) // prove proposition => proven theorem


However, you may use assumptions from a precondition locally in a function for optimization purposes without asserting the precondition first IFF:

1. the function is pure (no side effects)

2. the optimizer is capable of detecting inconsistencies and ignore user provided assumptions when a conflict arises.

3. no code makes assumptions based on the postconditions of the function

I think so, at least.

Walter Bright:

> I don't care if you make such remarks about me, but I do care about the level of discourse in the forum sinking to such levels. Please refrain from such.

Yes sorry, I have lost my temper when you have written "Or perhaps some people are just being argumentative. I can't really tell.". People in this thread are not argumentative for the sake of wasting time and energy.

Bye,
bearophile

On Friday, 1 August 2014 at 09:02:36 UTC, Walter Bright wrote:
> On 7/31/2014 11:24 PM, "Ola Fosheim Grøstad" <ola.fosheim.grostad+dlang@gmail.com>" wrote:
>> On Friday, 1 August 2014 at 02:44:51 UTC, Walter Bright wrote:
>>>> That entry makes no mention of assert being used as an optimization hint.
>>>>
>>> Saying that a predicate is always true means it's available to the optimizer.
>>
>> An assert does not say that the predicate is always true.
>
> Yes, it does. From Meyers' comprehensive tome on the topic "Object-Oriented Software Construction" (1997) where he writes:
>
> "A run-time assertion violation is the manifestation of a bug in the software."
>
>     -- pg. 346
>
> In fact, Meyers calls it "rule (1)" of assertions.

No, the statement in this quote does not imply that it is always true. It says that there is a bug if it isn't, which obviously wouldn't make any sense if the predicate were always true.

An assertion doesn't tell the compiler that a predicate is true, it tells the compiler to _check whether_ it is true.

On Friday, 1 August 2014 at 10:42:50 UTC, Marc Schütz wrote:
> On Friday, 1 August 2014 at 09:02:36 UTC, Walter Bright wrote:
>> On 7/31/2014 11:24 PM, "Ola Fosheim Grøstad" <ola.fosheim.grostad+dlang@gmail.com>" wrote:
>>> On Friday, 1 August 2014 at 02:44:51 UTC, Walter Bright wrote:
>>>>> That entry makes no mention of assert being used as an optimization hint.
>>>>>
>>>> Saying that a predicate is always true means it's available to the optimizer.
>>>
>>> An assert does not say that the predicate is always true.
>>
>> Yes, it does. From Meyers' comprehensive tome on the topic "Object-Oriented Software Construction" (1997) where he writes:
>>
>> "A run-time assertion violation is the manifestation of a bug in the software."
>>
>>    -- pg. 346
>>
>> In fact, Meyers calls it "rule (1)" of assertions.
>
> No, the statement in this quote does not imply that it is always true. It says that there is a bug if it isn't, which obviously wouldn't make any sense if the predicate were always true.
>
> An assertion doesn't tell the compiler that a predicate is true, it tells the compiler to _check whether_ it is true.

Even the WP article that you referred to says:
"An assertion may be used to verify that an assumption made by the programmer [...] remains valid"
https://en.wikipedia.org/wiki/Assertion_%28software_development%29#Assertions_for_run-time_checking

It may be used to _verify_ an assumption, not to _claim_ that it is true.

On Friday, 1 August 2014 at 04:51:06 UTC, eles wrote:
> assert(0) is a special contract that requires no code for its verification, as it obviously fails. This is why the compiler will always make it a halting point, in all builds."

This is wrong. As I have shown over in the other thread, the semantics Walter intended (and that are currently implemented in DMD, LDC and probably GDC) for assert(0) have nothing to do with what a false assertion would normally entail, but are merely a halt/abort/trap/… intrinsic.

Cheers,
David

On Friday, 1 August 2014 at 09:02:36 UTC, Walter Bright wrote:
> On 7/31/2014 11:24 PM, "Ola Fosheim Grøstad" <ola.fosheim.grostad+dlang@gmail.com>" wrote:
>> On Friday, 1 August 2014 at 02:44:51 UTC, Walter Bright wrote:
>>>> That entry makes no mention of assert being used as an optimization hint.
>>>>
>>> Saying that a predicate is always true means it's available to the optimizer.
>>
>> An assert does not say that the predicate is always true.
>
> Yes, it does. From Meyers' comprehensive tome on the topic "Object-Oriented Software Construction" (1997) where he writes:
>
> "A run-time assertion violation is the manifestation of a bug in the software."
>
>     -- pg. 346
>
> In fact, Meyers calls it "rule (1)" of assertions.

I would rephrase it as: "An assert says that either the predicate
is always true, or else the program is in an invalid state and will not operate correctly".

But I do think this entire argument seems to me to be rather misplaced. I think it's really it's about -release, not about assert().

The arguments presented by Ola et al mostly seem to be arguments against the use of the -release switch. Because it is a very dangerous flag.

If you're removing all your asserts I'd say you're playing a dangerous game already. If an assert would have failed, but execution continued anyway, you're in undefined behaviour -- at the very least, you're in a condition that the programmer believed could never happen.

If you are disabling your asserts, but still believe that they may fail, that means you're expecting your program to enter undefined behaviour! That seems to be a rather illogical position.

I think very strongly that we should rename the "-release" switch, especially if we do start to make use of asserts. It's going to cause no end of confusion and passionate debate.

---

In one of the 2013 DConf talks a lint tool was discussed that disallowed you from you writing a condition that was provably impossible based on 'in' contracts.
eg:

void foo( int x)
in{
   assert(x > 6);
}
body {
    if (x > 2)   // ERROR! This is always true!
    ...
}

Which is an interesting approach.

By definition, any optimisations that are performed on the basis of an assert() that could affect control flow, are detectable with 100% accuracy by a lint tool. And so, if you wanted to remove all your asserts but were worried about this issue, it's detectable at compile time.

On Friday, 1 August 2014 at 04:51:06 UTC, eles wrote:
>
> While in Debug mode

Generally decent, but I don't agree that the absence of -release implies debug mode.

-Wyatt

On Friday, 1 August 2014 at 11:53:28 UTC, Don wrote:
> I think very strongly that we should rename the "-release" switch, especially if we do start to make use of asserts. It's going to cause no end of confusion and passionate debate.

Pretty much summary of both threads.