On Saturday, 2 August 2014 at 02:42:50 UTC, Chris Cain wrote:
> On Saturday, 2 August 2014 at 02:32:45 UTC, Timon Gehr wrote:
>> On 08/02/2014 04:28 AM, Chris Cain wrote:
>>> ...
>>
>> I retract my apology.
>
> Of course. The worst curse I could wish upon you is that you stick to your guns. So stick to your guns, my friend. :-)

I don't know... maybe I can try to explain what he is trying to
say.
Correct me if I am wrong in either of your interpretations of
assert.

Your claim is that an assertion is a promise, by the person
asserting, that something is always true. Meaning if you assert
something, the compiler will interpret it to always be true. In
essence the compiler will interpret your promise(as the
programmer) as a never changing fact that can be used for
optimizations.

His claim is that an assertion is a claim by the person
asserting. That claim has not been proven to be true or false.
Meaning that as a claim, the compiler can't do anything with that
information alone. The compiler can try to check if the claim is
true and if it is, use that information to optimize. But if it is
not checked it is merely a claim with no backing, and as such,
nothing can be done with it.

...

Ok that was my interpretation of both of your interpretations. I
hope I didn't misinterpret.

Personally I side with the argument that assert is a claim which
I believe is closer to the actual meaning of the word assert and
closer to how programmers use assert now.

If you look at the google definition of assert...

"state a fact or belief confidently and forcefully."

You will see that it says an assertion is a statement of a "fact
or belief". The "confidently and forcefully" portion of the
definition is just describing the attitude of the asserter, so in
this context is not relevant. That means that the speaker can use
an assertion to state either a fact or a belief(I think in this
context a belief is sufficiently close to a claim, both could be
true or false). As the person being spoken to, there is no way to
know if the speaker is asserting a fact or a belief. This means
that as the person being spoken to, you have no choice but to
come to the conclusion that what is being asserted could be
either of the two and thus could either be true or false.

In the context of a programmer and a compiler, the programmer is
the speaker and the compiler is the thing being spoken to. This
means that if the programmer asserts something the compiler has
no choice but to interpret what is being asserted could either be
true or false.

Now you could say that the compiler implicitly trusts the
programmer and as such takes all assertions as fact, but I
believe that is a mistake on the compilers part. If the compiler
implicitly trusted the programmer, there would be no warnings,
and type checking ... ect. You could say that the compiler only
implicitly trusts the programmer in the case of assert, but I
still believe this to be a mistake on the compilers part.

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.

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

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

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, it's logical that it should, by default, accept what you say just like it accepts every other command you give it.

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

On 08/02/2014 06:28 AM, Timon Gehr wrote:
> On 08/02/2014 06:11 AM, Chris Cain wrote:
>> ...
>
>> So no, a statement of fact can be verifiable and still false by your
>> quote.
>
> It is possible that this is indeed what it tries to communicate. Thanks
> for bearing with me in any case!
>
> 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?

BTW: I missed something:

On 08/01/2014 11:18 PM, Chris Cain wrote:
> Imagine my surprise when I Google'd "assert definition" to find it meant
> "state a fact or belief confidently and forcefully."

On 08/02/2014 12:03 AM, Chris Cain wrote:
> Assertions are a statement of fact or belief and can be backed up with
> evidence.

Is 'making a statement of fact' really the same as 'stating a fact'?

On 08/02/2014 06:40 AM, Tofu Ninja wrote:
>
>
> Ok that was my interpretation of both of your interpretations. I
> hope I didn't misinterpret.

Your interpretation of my interpretation is exactly right. (However, note that I am not using this reasoning to say the new semantics are wrong, I am saying the new semantics are not obviously what was intended from the beginning once given the definition of 'assert' in English. This is what this discussion is about.)

On 8/1/14, 9:46 PM, 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.
>
>>
>>> 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. 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.
>
> `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. 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.
>
> 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, it's logical that it
> should, by default, accept what you say just like it accepts every other
> command you give it.
>
> 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. 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.

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

On Saturday, 2 August 2014 at 04:54:09 UTC, 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

I am glad our squabbling amuses you :)

On Saturday, 2 August 2014 at 04:40:53 UTC, Tofu Ninja wrote:
> I don't know... maybe I can try to explain what he is trying to
> say.
> Correct me if I am wrong in either of your interpretations of
> assert.
>
> Your claim is that an assertion is a promise, by the person
> asserting, that something is always true. Meaning if you assert
> something, the compiler will interpret it to always be true. In
> essence the compiler will interpret your promise(as the
> programmer) as a never changing fact that can be used for
> optimizations.

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

> His claim is that an assertion is a claim by the person
> asserting. That claim has not been proven to be true or false.
> Meaning that as a claim, the compiler can't do anything with that
> information alone. The compiler can try to check if the claim is
> true and if it is, use that information to optimize. But if it is
> not checked it is merely a claim with no backing, and as such,
> nothing can be done with it.

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.

>
> ...
>
> Ok that was my interpretation of both of your interpretations. I
> hope I didn't misinterpret.
>
> Personally I side with the argument that assert is a claim which
> I believe is closer to the actual meaning of the word assert and
> closer to how programmers use assert now.
>
> If you look at the google definition of assert...
>
> "state a fact or belief confidently and forcefully."
>
> You will see that it says an assertion is a statement of a "fact
> or belief". The "confidently and forcefully" portion of the
> definition is just describing the attitude of the asserter, so in
> this context is not relevant. That means that the speaker can use
> an assertion to state either a fact or a belief(I think in this
> context a belief is sufficiently close to a claim, both could be
> true or false). As the person being spoken to, there is no way to
> know if the speaker is asserting a fact or a belief. This means
> that as the person being spoken to, you have no choice but to
> come to the conclusion that what is being asserted could be
> either of the two and thus could either be true or false.
>
> In the context of a programmer and a compiler, the programmer is
> the speaker and the compiler is the thing being spoken to. This
> means that if the programmer asserts something the compiler has
> no choice but to interpret what is being asserted could either be
> true or false.
>
> Now you could say that the compiler implicitly trusts the
> programmer and as such takes all assertions as fact, but I
> believe that is a mistake on the compilers part. If the compiler
> implicitly trusted the programmer, there would be no warnings,
> and type checking ... ect. You could say that the compiler only
> implicitly trusts the programmer in the case of assert, but I
> still believe this to be a mistake on the compilers part.

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.

On Saturday, 2 August 2014 at 04:47:05 UTC, Timon Gehr wrote:
>
> BTW: I missed something:
>
> On 08/01/2014 11:18 PM, Chris Cain wrote:
>> Imagine my surprise when I Google'd "assert definition" to find it meant
>> "state a fact or belief confidently and forcefully."
>
> On 08/02/2014 12:03 AM, Chris Cain wrote:
>> Assertions are a statement of fact or belief and can be backed up with
>> evidence.
>
> Is 'making a statement of fact' really the same as 'stating a fact'?

Probably not. Maybe I wasn't rigorous with the first definition. That said, as far as the compiler is concerned when asserts are taken out, it's reasonable for it to just accept it as a fact even if it doesn't prove it as such. Because we're gods and all.

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.

On Saturday, 2 August 2014 at 04:54:09 UTC, 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

Oh by the way, how about the color of that bike shed! It really needs to be blue. :-p

Sorry :)