On Saturday, 2 August 2014 at 05:12:12 UTC, Tofu Ninja wrote:
> On Saturday, 2 August 2014 at 04:46:43 UTC, Chris Cain wrote:
>
>> No. You can verify it but find it to be false. Your proof would show it to be false. The fact that you can write a proof showing it to be false is a proof that it was verifiable in the first place.
>
> I think if one says they are going to prove something, they
> implicitly mean they are going to prove it to be true. And if one
> says they are going to disprove something, they implicitly mean
> they are going to prove it to be false.
>
> I think that might be causing a bit of misinterpretation.

True. If someone says they are *going* to prove something ...

If someone says I *can* prove it... well...

http://en.wikipedia.org/wiki/Handwaving

On 08/02/2014 06:46 AM, Chris Cain wrote:
> On Saturday, 2 August 2014 at 04:28:33 UTC, Timon Gehr wrote:
>> On 08/02/2014 06:11 AM, Chris Cain wrote:
>>> On Saturday, 2 August 2014 at 03:40:47 UTC, Timon Gehr wrote:
>>>> I already googled 'statement of fact' myself earlier, and found the
>>>> wikipedia entry for 'fact', that I quoted back then:
>>>> http://en.wikipedia.org/wiki/Fact
>>>>
>>>> "The usual test for a statement of fact is verifiability, that is,
>>>> whether it can be demonstrated to correspond to experience."
>>>>
>>>> I.e. in order to determine whether something is a statement of fact,
>>>> one should verify it. Do you agree that it is saying this?
>>>
>>> I'll just do this real quick, because it's a really easy one to show the
>>> problem with.
>>>
>>> Google "verifiable" ->
>>> http://www.merriam-webster.com/dictionary/verifiable -> "capable of
>>> being verified"
>>> ...
>>
>> Great, now we are getting somewhere.
>>
>> http://dictionary.reference.com/browse/verify?s=t
>>
>> "to prove the truth of, as by evidence or testimony; confirm;
>> substantiate: Events verified his prediction."
>>
>> I understand "capable of being verified" as "there is a way to verify
>> this" which is the same as "this can be proven" which would imply
>> "this is true".
>>
>> What's wrong here?
>
> The fact that you assume that something "can be proven" means it "has
> been proven" or "must be proven". Because you don't necessarily have to
> prove it, it doesn't necessarily mean it is true. It's a statement that
> you are suggesting is true but *could* be falsified/shown to be
> false/verified/verified to be false.
>
> The mere fact that asserts take in expressions show that something "can
> be proven", but there is no implication that it, therefore, must be
> proven. If you put an expression in an assert and it successfully
> compiles, you've made a statement of fact. It's useful that it is
> checked/proven in debug builds but not surprising that it's required to
> by definition.
> ...

Well, if there is no proof of something, how can I claim it can be proven? In fact, in my past life, when somebody told me something like '...and actually one _can prove_ that any non-planar graph contains either a K_5 or a K_{3,3} as a minor', then this invariably meant that there exists a proof, but that they will not tell me the proof now.

Words are strange; apparently it is very common that they don't mean similar things to different people. Isn't it possible, that 'verifiable' just has an idiomatic usage that does not represent the obvious meaning derived from 'verify'? Or is 'verify' bivalent like that as well?


>>
>>> That is, it's something that has some ability to be verified. Thus, 1==2
>>> is "verifiable" (it can be shown to be either true or false).
>>> ...
>>
>> If I can verify 1==2, I would prove 1==2, as per the definition above,
>> no?
>
> No.

The definition above was:

"to prove the truth of, as by evidence or testimony; confirm; substantiate: Events verified his prediction."

> You can verify it but find it to be false. Your proof would show it
> to be false. The fact that you can write a proof showing it to be false
> is a proof that it was verifiable in the first place.
>
>> It is possible that this is indeed what it tries to communicate.
>> Thanks for bearing with me in any case!
>
> No problem. :)
>
>> But as I wrote in my previous post, now this brings up the issue that
>> if an assertion is a statement of fact, then it is not necessarily true.
>>
>> Why is it now obvious that it should be considered true?
>
> For the same reason that all of the other things you type into a program
> is accepted by a program.
> ...

I see.

> `if(...)` ... would it be strange if your program doubted that you
> really want to execute the block the if statement refers to? Of course
> it would.
>
> Basically, you're a god and what you say to do is law in computer
> programming.

(Except if you do something that's 'invalid', at which point all your carefully crafted laws get ignored immediately.)

> By default you expect the computer to not doubt you and to
> follow what you say. It's not like a person who will question your
> assertions and ask you to prove them or double check them for you.
> ...

For me, having them double checked is the main motivation for writing down assertions. I like failing assertions when they occur. They often almost immediately tell me what I screwed up, or which prior assumptions no longer hold and which code therefore I might need to modify in order to complete the implementation of a new feature. I personally don't want the compiler to trust me regarding those issues, and that's the whole point. This is how assert works in other languages and also how it works in current D compilers. However, whenever I write an assertion down, it is still a statement of fact/opinion/whatever, and more importantly, I feel strongly about that it should be true.

I don't think that if I had looked up 'assert' in a dictionary, I would have recognised an opposition between the definition in the dictionary and the 'old' semantics as described above.

> Though, the fact that it will double check them for you is helpful in
> debug builds, so it's an obvious enhancement for debugging purposes.
>
> Since assert is you making a statement of fact,

Note that it might just as well be a command that makes the program make a statement of fact.

> it's logical that it
> should, by default, accept what you say just like it accepts every other
> command you give it.
> ...

Yes, but what I say is: "I assert this." And _I_ do. If I do just this, this does not determine what _the compiler_ is to make of it. We need a separate operational semantics which IMO is not obvious a priori given just the definition in English and knowledge about programming without anything concerning 'assert'.

> If you're wrong... well, it's just like if you're wrong about your if
> statements or if you call the wrong function or pass in the wrong
> variables.

There is a distinct flavour to it. If I am wrong about an 'if' statement, I will still be able tell how the program will behave by inspecting the source code (if there is no other source of UB), whereas the new assert semantics deny me this possibility. I.e. my opinion is that "it's just like" is an exaggeration, also because it is not me testing the 'if' condition, but there it is obviously the program who is commanded to do it.

> You'll get incorrect program behavior. Unlike those other
> things, since it's verifiable, there exists some sort of configurations
> where the program can be helpful to you by verifying your assertions.

Type checking will be performed even in -release builds.
I guess it is hard to reach consensus from here?

On 08/02/2014 06:54 AM, Andrei Alexandrescu wrote:
>
> I don't think there's ever been a more majestic thread in the history of
> this forum. Probably up there with the best of them anywhere and
> anytime. It's become officially an Epic Debate.
>
> Andrei

Wait, does this thread outclass the @property debates?
We should discuss @property again soon!

On 08/02/2014 05:34 AM, Andrew Godfrey wrote:
> Suppose I call some logging function which has a faulty assertion in it.
> What about Walter's position prevents that assertion's effects from
> escaping the logging function and infecting my code?

Nothing. Undefined behaviour is completely non-modular.

> I know cross-module
> optimization is hard hence this may be unlikely,

Inlining may happen.

> but still it shows
> something missing.
>
> I know Walter has said repeatedly that at this point the program is
> invalid, Implying that it deserves whatever happens to it. I suspect
> this is a subtopic we should be discussing more directly. What are the
> boundaries?

The semantics that are proposed to be pulled into the language spec are currently summarized as:

- In non-release mode, an assertion failure will abort the program (maybe by throwing an Error).

- In release mode, an assertion failure leads to undefined behaviour.

I.e. I think there aren't any 'boundaries', unless I am misunderstanding this term.

On Saturday, 2 August 2014 at 05:07:58 UTC, Chris Cain wrote:

> Actually, I'm going to clarify this: Your assertion is *not* the promise. Your assertion is simply a statement of fact (note, that does not mean it's a fact, as that appears to be a point of confusion: a statement of fact is simply a statement that *can* be verified).

I am going to have to disagree, I think what you are calling a
statement of fact, is actually a claim. A statement is simply a
piece of communication. So if you state a belief, you are simply
communicating that belief's existence. So a statement of fact is
simply the communication that the fact exists.

In reality you can never actually state a fact because you can
only ever believe a fact is true. It comes down to the
philosophical problem of "I think therefore I am", which
basically says that the only thing that your mind can PROVE 100%
is that you are thinking.

You can state a belief, but to anyone else hearing that
statement, it will be a claim. Basicly is comes down to this...

*A claim is something that can be true or false

*A belief is a claim that is true in the believer's mind, but if
stated becomes a claim due to that possibility that the
believer's is in error

*A fact is something that is always true

That is why you can have true statements and false statements, it
is not that the statement is self is true or false, but that the
claim that is being stated is true or false.

> An intrinsic part of programming is that whatever you write is what you intend to write (that is, it must assume that you aren't incorrect because it otherwise couldn't compile the program ... or it'd have to ask you for every line to "sign off" that it's what you intended). The obvious conclusion is that you must "promise" that you know what you're doing.
>
> As the human and good programmer, it seems that you wouldn't want to assume you're correct, but the compiler/programming language itself has no option but to assume you meant an if statement there or a function call here, and that you intended these particular arguments to be passed in this particular order. It also assume your assertions are what you meant them to be. The fact that they are checked is a bonus feature (which is really where the confusion behind assertions lies, as it was for me... I, like you, thought that assertions MUST be verified and checked, but that turns out to not be what that meant at all).


It is not a matter of the compiler trying to determine if you
meant to write what you did or not(there is no way it can). It is
a matter of the compiler determining if what you wrote is what it
considers to be correct input. If you try to compile
"SDA@#$!$SDF#$T#", the compiler has no way of knowing if you
meant to write that or not, but it is still allowed to reject
that.

> Of course, I can understand that interpretation. But at the same time, why would you write something and expect a compiler to do nothing with it? Is there any other construct in the language that does that? Even noops in ASM which literally mean "do nothing" actually have an effect on the intended meaning of a program.

Because if the compiler actually checks the claim then it can
optimize on it, but if the compiler does not check then it can
not know its true and can not optimize.

> I see it the exact opposite way. I see it as the compiler is helpful and will do as much proving as it can, but ultimately it must always logically put if statements in where you want them and function calls in where you want them. Technically, it takes some liberties with optimizations because it has good reason to believe that the two interpretations are equivalent. That said, when we pass `-O` to the compiler, we're commanding it to do that... so... *shrug*
>
> Thus when you assert something is true and the compiler can't immediately disprove you, it must follow what you say. FWIW, I feel that something like this should fail compilations:
>
> ```
> int x = 1;
> assert(x != 1);
> ```
>
> because the compiler could, in fact, disprove you at compile time. That said, it's not a scalable approach because there exists too many programs that you cannot prove the output of. Otherwise, if it can't immediately disprove what you say (by type checking, for instance), then it has no choice but to do what you say, even if you're wrong. Even if you do `x1 == x2 && y1 == x2` in a conditional somewhere, it can't/won't take liberties to "correct it" to `x1 == x2 && y1 == y2`. But if x1 is a FloatMeters and x2 is a FloatMiles, I would expect it to disprove that it's a correct comparison (unless you make statements suggesting that this is what you really mean, of course). But then again, I refer to the above where obviously illogical things should fail to compile as well. But once it compiles, I expect that it does what I say even if what I say is wrong.

I think a point that needs to be addressed is that there is a
difference between a program being defined incorrectly and a
program being undefined.

If the programmer defines his program incorrectly, then yes, you
are correct in that the compiler has no choice but to still take
the incorrect definition.
The program is still defined in a way the compiler understands,
its just not what the programmer was trying to say.

But, if a program is undefined, then the compiler does not know
what to do, which in how compilers are implemented means the
compiler can literally do anything it wants.

Typing "while" instead of "if" might be an incorrect definition
of the program that the programer was trying to create, but is is
still a valid program definition(just not the one the programmer
wanted).

On the other hand, having contradicting asserts(with your
interpretation of assert) is not an incorrectly defined program,
but an undefined program because it simply does not make sense.

On Saturday, 2 August 2014 at 05:32:43 UTC, Timon Gehr wrote:
> Well, if there is no proof of something, how can I claim it can be proven? In fact, in my past life, when somebody told me something like '...and actually one _can prove_ that any non-planar graph contains either a K_5 or a K_{3,3} as a minor', then this invariably meant that there exists a proof, but that they will not tell me the proof now.
>
> Words are strange; apparently it is very common that they don't mean similar things to different people. Isn't it possible, that 'verifiable' just has an idiomatic usage that does not represent the obvious meaning derived from 'verify'? Or is 'verify' bivalent like that as well?

It seems to be exactly as Tofu suggested. I don't really know exactly how to explain to you that the concept of verifiability/falsifiability does not mean that something will verify as true or be falsified just to assert that they have an ability of being shown to be false or shown to be true (that is, there needn't be a proof in hand or even discovered, just that some proof could be written about it's truth or falseness, even if it has never been discovered).

In the world of science in general, "falsifiability" is clearly used for any research. It means "able to be proven false", of course, but if that implied it wasn't true, then it would mean that all science is false which is truly a bizarre conclusion.

http://en.wikipedia.org/wiki/Falsifiability

^^ See? It's an important part of science that there is the possibility of proving it false. That *doesn't* imply it *is* false, though. Likewise for verifiability (they're really just synonyms, which should really show you that there actually existing both a proof for truth and falseness doesn't make sense)

http://www.synonym.com/synonyms/falsifiable/ -> verifiable is a synonym.

> For me, having them double checked is the main motivation for writing down assertions. I like failing assertions when they occur. They often almost immediately tell me what I screwed up, or which prior assumptions no longer hold and which code therefore I might need to modify in order to complete the implementation of a new feature. I personally don't want the compiler to trust me regarding those issues, and that's the whole point. This is how assert works in other languages and also how it works in current D compilers. However, whenever I write an assertion down, it is still a statement of fact/opinion/whatever, and more importantly, I feel strongly about that it should be true.
>
> I don't think that if I had looked up 'assert' in a dictionary, I would have recognised an opposition between the definition in the dictionary and the 'old' semantics as described above.

I could see that. That said, I was on the opposite side of the fence. I knew the dictionary understanding but simply separated the concepts in my head before. I thought of the assert in programming languages as you currently do. However, this thread has shown me that they were always intended to be the same, and it's significantly clarified (for me) where I would use assertions and where I'd use enforcements, for instance (the boundry has always been pretty fuzzy to me... "use asserts for the purpose of program bugs" has always been somewhat unclear).

I guess not everyone knew and understood the dictionary definition, so it seems that my point wasn't originally helpful.

> Note that it might just as well be a command that makes the program make a statement of fact.

That's pretty much exactly what I think it's intended to be. Except I'd tweak it to say that it's a command that you use to make a statement of fact (the program isn't doing anything).

> There is a distinct flavour to it. If I am wrong about an 'if' statement, I will still be able tell how the program will behave by inspecting the source code (if there is no other source of UB), whereas the new assert semantics deny me this possibility. I.e. my opinion is that "it's just like" is an exaggeration, also because it is not me testing the 'if' condition, but there it is obviously the program who is commanded to do it.

Sure. A bit of a different flavor, but essentially the same. Incorrect statements make incorrect program behavior (in the case of assert, I think understanding the real meaning behind it will make it far easier to reason about ... "UB" isn't quite accurate as the meaning behind what you say has a clear implication of what type of behavior will follow, it's just that currently the optimizer doesn't do all it could do)

>
>> You'll get incorrect program behavior. Unlike those other
>> things, since it's verifiable, there exists some sort of configurations
>> where the program can be helpful to you by verifying your assertions.
>
> Type checking will be performed even in -release builds.
> I guess it is hard to reach consensus from here?

Well, there's a not-so-subtle difference between type checking and assertions. Whereas assertions could only be checked at runtime, failing to use typechecking in a statically compiled program means that you simply couldn't compile the program to begin with.

I'd like to reiterate that I think it would be better if the compiler COULD prove some assertion impossible at compile time, then it should.

e.g.

```
int x = 1;
assert(x != 1);
```

... It'd be reasonable for this to fail to compile. Frankly, this could unify static assert and assert (though, I'm not sure if I'd feel comfortable with this... I'd, after all, prefer a static foreach and I'd also like to keep my static ifs because I'd like to enforce that these things are always handled at compile time).

On Saturday, 2 August 2014 at 06:09:42 UTC, Chris Cain wrote:

> Sure. A bit of a different flavor, but essentially the same. Incorrect statements make incorrect program behavior (in the case of assert, I think understanding the real meaning behind it will make it far easier to reason about ... "UB" isn't quite accurate as the meaning behind what you say has a clear implication of what type of behavior will follow, it's just that currently the optimizer doesn't do all it could do)

Not a different flavor, fundamentally different things, see my
other post.

On Saturday, 2 August 2014 at 06:08:43 UTC, Tofu Ninja wrote:
> On Saturday, 2 August 2014 at 05:07:58 UTC, Chris Cain wrote:
>
>> Actually, I'm going to clarify this: Your assertion is *not* the promise. Your assertion is simply a statement of fact (note, that does not mean it's a fact, as that appears to be a point of confusion: a statement of fact is simply a statement that *can* be verified).
>
> I am going to have to disagree, I think what you are calling a
> statement of fact, is actually a claim. A statement is simply a
> piece of communication. So if you state a belief, you are simply
> communicating that belief's existence. So a statement of fact is
> simply the communication that the fact exists.

Well, you can disagree but it doesn't change the fact that what I meant and what you're saying are two different things. With this knowledge you can now infer that you are putting forth effort to intentionally misunderstand me despite me trying to clarify that there is a difference, which isn't productive.

> In reality you can never actually state a fact because you can
> only ever believe a fact is true. It comes down to the
> philosophical problem of "I think therefore I am", which
> basically says that the only thing that your mind can PROVE 100%
> is that you are thinking.
>
> You can state a belief, but to anyone else hearing that
> statement, it will be a claim. Basicly is comes down to this...
>
> *A claim is something that can be true or false
>
> *A belief is a claim that is true in the believer's mind, but if
> stated becomes a claim due to that possibility that the
> believer's is in error
>
> *A fact is something that is always true
>
> That is why you can have true statements and false statements, it
> is not that the statement is self is true or false, but that the
> claim that is being stated is true or false.

Frankly, it seems we've regressed back to making up definitions for words and phrases that are well-defined and those well-defined meanings contradict what you're trying to suggest. That's not going to help you understand why I think assert makes sense given the real definition of an assertion.

> It is not a matter of the compiler trying to determine if you
> meant to write what you did or not(there is no way it can). It is
> a matter of the compiler determining if what you wrote is what it
> considers to be correct input. If you try to compile
> "SDA@#$!$SDF#$T#", the compiler has no way of knowing if you
> meant to write that or not, but it is still allowed to reject
> that.

Of course, but it must reject that because it couldn't possibly understand that. Furthermore, most of the things in compilers that are disprovable at compile time are disproven at compile time. Those things which cannot be disproven at compile time (see: halting problem) cannot be rejected. Hence, if statements and asserts, and why type-check failures result in a failed compilation.

> Because if the compiler actually checks the claim then it can
> optimize on it, but if the compiler does not check then it can
> not know its true and can not optimize.

But it doesn't need to check because that's not what assert means to do. You're focusing too much on the "checking" part which has nothing to do with the actual English definition of assert (which is my point for why it makes sense for assert to do what it does). A runtime check is a "nice thing to have" (it makes asserts more useful, ultimately), but it seems completely orthogonal to what assert means in this case considering the definition of assert.

> I think a point that needs to be addressed is that there is a
> difference between a program being defined incorrectly and a
> program being undefined.
>
> If the programmer defines his program incorrectly, then yes, you
> are correct in that the compiler has no choice but to still take
> the incorrect definition.
> The program is still defined in a way the compiler understands,
> its just not what the programmer was trying to say.
>
> But, if a program is undefined, then the compiler does not know
> what to do, which in how compilers are implemented means the
> compiler can literally do anything it wants.
>
> Typing "while" instead of "if" might be an incorrect definition
> of the program that the programer was trying to create, but is is
> still a valid program definition(just not the one the programmer
> wanted).
>
> On the other hand, having contradicting asserts(with your
> interpretation of assert) is not an incorrectly defined program,
> but an undefined program because it simply does not make sense.

OK, but I see these as being much more similar conceptually than you're giving them credit. Despite "undefined behavior" occurring when an assertion fails, it doesn't actually mean that you can't reason about what can occur, just that there's no required definition for what will occur (that's why it's called "undefined"). That is the two interpretations of a D program are accepted by the spec:

```
assert(x != 1);
//... code that doesn't have any effect on x
if(x == 1) { /* ... */ }
```

```
assert(x != 1);
//... code that doesn't have any effect on x
```

The "undefined behavior" is that it allows these two to be equivalent programs. You can reason about why the program isn't doing what you want, so it's not that it's an "undefined program", just that two (or more) definitions of a program are equivalent as far as the D spec is concerned.

You don't know which one you can get, but you do know that they are equivalent (because of your assertion).

Actually, what's really weird is the fact that no one would be complaining if asserts were always checked, even though the above is exactly what you could get by the optimizer. The real strange thing is that you'd want the removal of checked asserts to change the way your program can be optimized.

On 08/02/2014 08:09 AM, Chris Cain wrote:
> On Saturday, 2 August 2014 at 05:32:43 UTC, Timon Gehr wrote:
>> Well, if there is no proof of something, how can I claim it can be
>> proven? In fact, in my past life, when somebody told me something like
>> '...and actually one _can prove_ that any non-planar graph contains
>> either a K_5 or a K_{3,3} as a minor', then this invariably meant that
>> there exists a proof, but that they will not tell me the proof now.
>>
>> Words are strange; apparently it is very common that they don't mean
>> similar things to different people. Isn't it possible, that
>> 'verifiable' just has an idiomatic usage that does not represent the
>> obvious meaning derived from 'verify'? Or is 'verify' bivalent like
>> that as well?
>
> It seems to be exactly as Tofu suggested. I don't really know exactly
> how to explain to you that the concept of verifiability/falsifiability ...

I actually knew and used falsifiable in this way you suggest. :)
I still don't think that if I falsify a statement, that I might actually have proven it true though.

>
> http://en.wikipedia.org/wiki/Falsifiability
>
> ^^ See?

"A statement is called falsifiable if it is possible to conceive an observation or an argument which proves the statement in question to be false."

If we have proven the statement true, we won't readily deem it possible to conceive an observation or argument which proves the statement in question to be false.

> It's an important part of science that there is the possibility
> of proving it false.

Not exactly. The article is stating that it should be conceivable that there might be an argument or an observation proving it false. But that often holds simply because we cannot prove properties of reality to hold. It is conceivable that gravity will not exist tomorrow and this would falsify many theories of physics. I don't really believe that this will happen, but it is conceivable.

> That *doesn't* imply it *is* false, though.
> Likewise for verifiability (they're really just synonyms, which should
> really show you that there actually existing both a proof for truth and
> falseness doesn't make sense)
>
> http://www.synonym.com/synonyms/falsifiable/ -> verifiable is a synonym.
> ...

Thanks! My hypothesis that verifiable/falsifiable are just idioms not extending to verify/falsify is not shattered by this though.

> .. I knew the dictionary understanding but simply separated the concepts in
> my head before. I thought of the assert in programming languages as you
> currently do. However, this thread has shown me that they were always
> intended to be the same, and it's significantly clarified (for me) where
> I would use assertions and where I'd use enforcements, for instance (the
> boundry has always been pretty fuzzy to me... "use asserts for the
> purpose of program bugs" has always been somewhat unclear).
> ...

I would actually agree with applying this reasoning for usage to 'old' assertions.

> ...
>
> Sure. A bit of a different flavor, but essentially the same. Incorrect
> statements make incorrect program behavior (in the case of assert, I
> think understanding the real meaning behind it will make it far easier
> to reason about ... "UB" isn't quite accurate as the meaning behind what
> you say has a clear implication of what type of behavior will follow,
> it's just that currently the optimizer doesn't do all it could do)
> ...

The type of behaviour that will follow (or indeed, precede the assertion) is dependent on whether or not the assertion may fail. If it may fail, UB will come and maybe eat your program, and chances are you won't notice immediately what happened. I guess we just disagree on the importance of this point.

> ...
>
> I'd like to reiterate that I think it would be better if the compiler
> COULD prove some assertion impossible at compile time, then it should.
>
> e.g.
>
> ```
> int x = 1;
> assert(x != 1);
> ```
>
> ... It'd be reasonable for this to fail to compile. Frankly, this could
> unify static assert and assert (though, I'm not sure if I'd feel
> comfortable with this... I'd, after all, prefer a static foreach and I'd
> also like to keep my static ifs because I'd like to enforce that these
> things are always handled at compile time).

It is not so clear where to draw the boundaries. In some languages you may need to prove the assertion true in order for it to pass the type checker.

On Saturday, 2 August 2014 at 05:59:14 UTC, Timon Gehr wrote:
> On 08/02/2014 05:34 AM, Andrew Godfrey wrote:
>> Suppose I call some logging function which has a faulty assertion in it.
>> What about Walter's position prevents that assertion's effects from
>> escaping the logging function and infecting my code?
>
> Nothing. Undefined behaviour is completely non-modular.
>
>> I know cross-module
>> optimization is hard hence this may be unlikely,
>
> Inlining may happen.
>
>> but still it shows
>> something missing.
>>
>> I know Walter has said repeatedly that at this point the program is
>> invalid, Implying that it deserves whatever happens to it. I suspect
>> this is a subtopic we should be discussing more directly. What are the
>> boundaries?
>
> The semantics that are proposed to be pulled into the language spec are currently summarized as:
>
> - In non-release mode, an assertion failure will abort the program (maybe by throwing an Error).
>
> - In release mode, an assertion failure leads to undefined behaviour.
>
> I.e. I think there aren't any 'boundaries', unless I am misunderstanding this term.

So even if the assertion is incorrect and the code is correct, the caller's correctness can be compromised? This seems impractical. As in, no one will in good conscience turn it on, except when their program is very small.