On Friday, 1 August 2014 at 11:53:28 UTC, Don wrote:
> The arguments presented by Ola et al mostly seem to be arguments against the use of the -release switch. Because it is

No, I think I do understand where Walter is coming from now. I remember some of the incomprehensible lectures I attended as a student where the entire blackboard was filled with quantors this and that.

I have spent hours every day the past few days thinking about how to explain it efficiently. I think D will benefit greatly if Walter dig into some of the theories on formal program verification, but everybody has to take rounds of the heuristic cycle to truly get down to it. So it is good that he does not accept it without an argument.

It is just not a topic where you can read one article and you will shout "eureka!". So I don't think it is a good idea to just say "oh it is just about -release". It is basically about finding common ground where program verification gets the best treatment possible and in a manner that is consistent with how users with a CS background perceive correctness.


I hope this gets us closer to common ground:


Let's assume with have a simple program like this:

int program(immutable string input){
	int r = input.length + input.length;
	assert(r == 2* input.length);
	return r;
}


Then execute it:
interpreter> run program "hi"


Then we have the following situation iff it completes successfully:

PROVEN:
if input=='hi' then input.length + input.length == 2* input.length

EQUIVALENT TO:

(input != 'hi') || (input.length + input.length == 2* input.length)


NOT PROVEN YET:
input.length + input.length == 2* input.length for all input != 'hi'


That basically means that a formal assert(x) and a runtime check has the following relationship:

runtime_assert(x) is the same as formal_prove( input!=ACTUALINPUT || x )

formal_assert(x) is the same as formal_prove(x)

Am 01.08.2014 05:17, schrieb Walter Bright:
>
> Frankly, it never occurred to me that it wasn't obvious. When something
> is ASSERTED to be true, then it is available to the optimizer. After
> all, that is what optimizers do - rewrite code into a mathematically
> equivalent form that is provably the same (but cheaper to compute). Its
> inputs are things that are known to be true.
>
> For example, if a piece of code ASSERTS that x is 3, thereafter the
> optimizer knows that x must be 3. After all, if the optimizer encounters:
>
>     x = 3;
>
> do I need to then add a note saying the optimizer can now make use of
> that fact afterwards? The use of "assert" is a very strong word, it is
> not "maybe" or "possibly" or "sometimes" or "sort of".
>
> When you write:
>
>     assert(x == 3);
>
> then at that point, if x is not 3, then the program is irretrievably,
> irredeemably, undeniably broken, and the default action is that the
> program is terminated.
>
> The idea expressed here by more than one that this is not the case in
> their code is astonishing to me.
>

Well, this all sounds sane and makes sense in a way.

The thing is, I never considered assert() to mean this up to now, which is probably influenced by the following reasons:

In programming I've always encountered assert() in an "check if assertions are enabled/you're in debug mode, do nothing otherwise" way (that's what C, C++, Java and Python do).

In unit tests the "checks" are also often called assertions.

I'm not a native speaker..
.. but even if I were: words used for constructs/function-names/... in programming often don't 100% match their "real" meaning (as used in human communication)[1] - why should it be different for assert(), especially when not implemented/used like that in many popular programming languages?


Cheers,
Daniel

[1] Examples for "spoken meaning" vs "programming lingo":
* or (in spoken language often used meaning "xor" - "do you want milk or sugar with your coffee?" - "true" - "wtf?")
* class (has many meanings in language, I guess none 100% matches the use in programming)
* peek()/poke() (which thankfully get more descriptive names in D)
* heap (the data structure has some kind of order, real life heaps are just chaotic piles of stuff)
* iota (just some greek letter, /maybe/ "a little bit" in spoken language, in some programming languages/std libs it means "sequence of consecutive numbers" - wtf?)
* exception (in real life not something that is "thrown around")

Am 01.08.2014 05:27, schrieb Walter Bright:
> On 7/31/2014 1:11 PM, Daniel Gibson wrote:
>> I guess in many cases I'd avoid using assert() in fear of breaking my
>> defensively written program (like that example from earlier: assert(x
>> !is null);
>> if(x) { x.foo = 42; }).
>
> I just hang my head in my hands at that code :-)
>
> Really, you're much better off writing something like:
>
>     if (x) {
>        x.foo = 42;
>     }
>     else {
>        writeln("Sack the QA dept. for not testing this code");
>        abort();
>     }
>
> which expresses what you intend directly and would be perfectly fine.
>

Not exactly - in release mode I don't want it to abort.

But it could be rewritten as
if(check(x != null, "Sack the QA dept. for not testing this code")) {
    x.foo = 42;
}

where check throws in debug mode and returns false in release mode if the condition fails.

I just never considered assert() to have the meaning you're giving it, even though maybe it was always considered to be like that but just not implemented "properly" by common languages. I wrote a bit more about this in another reply.

Cheers,
Daniel

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

This is offensive on more than one level. -- Andrei

On 08/01/2014 01:53 PM, Don 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.
>
> 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".
> ...

Bertrand _Meyer_ is not a furious proponent of undefined behaviour. He is not exactly a fan of C or C++ either and an expressed opponent of the typical 'C hacker' attitude.

> 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.

Sure, and it is /obviously/ perfectly fine to e.g. kill a tightrope walker, so this should not be prosecuted.

> If an assert would have failed, but execution continued
> anyway, you're in undefined behaviour

No. For the purpose of (maybe remote!) debugging, the programmer wants the behaviour to be _the one that the program specifies_, even if it is not the one that he _expected_.

> -- at the very least, you're in a
> condition that the programmer believed could never happen.
> ...

Yes, a condition that _some_ programmer believed could never happen. It is not even a given that this condition is not actually created somewhere and handled somewhere else, especially as software evolves.

> If you are disabling your asserts, but still believe that they may fail,
> that means you're expecting your program to enter undefined behaviour!

Nonsense. This claim is ignoring the current reality of software development. One would be expecting one's program to be buggy, but one would still think that _almost all_ assertions pass always and those that don't would be expected to pass _almost always_. How many pieces of non-trivial bug-free software did you write or _were required to work on without full knowledge about the code base_?

In any case if one is _disabling_ one's asserts, one doesn't expect them to have any kind of effect whether they may fail or not.

> That seems to be a rather illogical position.
>

It was constructed to seem to be. For example, the expectation that some asserts are wrong was conveniently replaced by the expectation that all (or at least a murkily unspecified amount of) asserts are wrong and the existence of trade-offs was ignored. This is simply a straw man used to defend an indefensible 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.
>
> ---

Disabling assertions and contracts and using them for optimization should be distinct options.

>
> 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.

By a family of lint tools indexed by the respective compiler back-ends. Furthermore, you have to understand all of those back-ends and all their passes completely and you need to track how information relating possible optimizations flows through them. You will not write all those lints in a lifetime and you need to start this undertaking again whenever someone writes a new back-end and you need to always keep the lints in sync with the back-ends (and maybe, front-ends). Besides, it is an incredibly complex solution for a completely trivial issue.

> And so, if you wanted to remove all your
> asserts but were worried about this issue, it's detectable at compile time.
>

This issue does not only affect people who are worried about it (and I'd guess the truth is way closer to the opposite), and in fact you yourself claimed above that it only affects people who are not worried about undefined behaviour. This is a rather illogical position to be in, even if both of the contradicting claims are not true statements. (Sorry! Couldn't resist! :-) )

In any case, please don't ignore existing complexity in order to make claims that seem pragmatic.

On 08/01/2014 11:02 AM, 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.

Sure, and _Meyer_'s "rule (1)" of software must therefore be that it contains no bugs, no?

On 8/1/14, 8:28 AM, Timon Gehr wrote:
>On 08/01/2014 01:53 PM, Don wrote:
>> If you are disabling your asserts, but still believe that they may fail,
>> that means you're expecting your program to enter undefined behaviour!
>
> Nonsense. This claim is ignoring the current reality of software
> development. One would be expecting one's program to be buggy, but one
> would still think that _almost all_ assertions pass always and those
> that don't would be expected to pass _almost always_. How many pieces of
> non-trivial bug-free software did you write or _were required to work on
> without full knowledge about the code base_?
>
> In any case if one is _disabling_ one's asserts, one doesn't expect them
> to have any kind of effect whether they may fail or not.

This doesn't ring true at all in the circles I frequent. I'm with Don. -- Andrei

On 08/01/2014 05:18 AM, Walter Bright wrote:
> On 7/31/2014 12:46 PM, H. S. Teoh via Digitalmars-d wrote:
>> AFAIK, the compiler currently doesn't use assert as a source of
>> information for optimization, it's just being proposed.
>
> It already does by default,

That's good and that's obviously not a problem. If the check is there, the behaviour of the optimized code does not change.

> the proposal is to do it for -release.
>

(I think he is talking about -release.)

On 08/01/2014 05:17 AM, Walter Bright wrote:
> On 7/31/2014 12:37 PM, Daniel Gibson wrote:
>> Am 31.07.2014 21:19, schrieb Walter Bright:
>>> That's the way assert in C/C++ conventionally worked. But this is
>>> changing. Bearophile's reference made it clear that Microsoft C++ 2013
>>> has already changed, and I've seen discussions for doing the same with
>>> gcc and clang.
>>
>> This will break so much code :-/
>
> Maybe you're right.

He is.

> I've always thought that assert() was a simple and
> obvious concept,

It is.

> and am genuinely surprised at all the varied (and even
> weird) interpretations of it expressed here.

Don't throw them all in one bag.

> I've never heard such
> things in my 30+ years of using assert().
>
> I have seen some misuse of assert() before, but the author of them knew
> he was misusing it and didn't have an issue with that.
>
> I can't even get across the notion of what a program's inputs are. Sheesh.
> ...

You didn't try. You were obviously being misunderstood and just repeated the same wording.

> Or perhaps some people are just being argumentative. I can't really
> tell. I can tell, however, than many of these sub-threads have ceased to
> contain any useful discussion.

Are you now trying to generalize over opinions that are not your own as wrong by only refuting some of them?

All the fallacious reasoning you have put forward in this thread is really tiring. Please don't ignore logic.

On 08/01/2014 05:29 AM, Walter Bright wrote:
> On 7/31/2014 12:48 PM, bearophile wrote:
>> I am against the idea of turning asserts into a dangerous
>> assert-assume hybrid.
>> And you have ignored some answers by Timon and others.
>
> Every post I answer spawns 5 more responses.

I am sorry but your posts were not constructed carefully enough to not warrant rebuttals.

> It's exponential.

I won't count posts now, but I think that this is not true.

> At some point, I have to give up.

Saying that you are obviously right and other people are maybe just argumentative is not 'giving up'.

> I've spent 2 days on this.

Everyone has.