On 08/02/2014 08:40 AM, Andrew Godfrey wrote:
>
> So even if the assertion is incorrect and the code is correct, the
> caller's correctness can be compromised?

Yes. The reasoning is that if the assertion is incorrect, the program is fundamentally broken, it enters an invalid state and hence it is fair game to make the behaviour undefined.

> This seems impractical. As in,
> no one will in good conscience turn it on, except when their program is
> very small.

That was my reasoning as well, but it wasn't universally agreed with.

On Saturday, 2 August 2014 at 06:36:00 UTC, Timon Gehr wrote:
>> 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.

Perhaps I just don't understand what you're getting at. It seems throughout that you are thinking "statements of fact" has a meaning that it's inherently true and is proven or must be proven.

It seems to me that you've suggested:

If falsifiable -> can be proven to be false -> must be proven false -> is false
and
If verifiable -> can be proven to be true -> must be proven true -> is true

(falsifiable == verifiable)
(can be proven to be false == can be proven to be true)
(false == true) is trivially false.

Which must be conclusive that verifiability/falsifiability doesn't imply true/false.

Thus, an assertion is a statement of fact, something which can be proven true (or false). It does not mean that you must prove it to be true for it to be an assertion. When you assert something, you're communicating a statement of fact. If you communicate a statement of fact to a compiler, what do you expect it to do? Ignore you, like it ignores your if-statements and function calls? Oh, it doesn't do that, so the obvious conclusion is that it will take your statement of fact and use it for something semantically meaningful. What is semantically meaningful about a statement of fact by a programmer? He hasn't demanded you check it or anything, he's just said something. Logically, the only thing it could do is try to use what you have said in some way. Ultimately, it makes total sense that it could effect the optimization passes.

It happens to be nice that when you don't care about performance, the compiler will double check your assertions. But when you do care about performance, assertions being checked (which isn't really what you've asked for) is not ideal.

There's literally no more ground to be covered here.

I feel it's abundantly obvious that asserts should work this way given the definition of asserts. If you disagree with my conclusion, I don't think there's any more that we can communicate to each other about it. I totally understand why you think asserts meant that you wanted the compiler to check before (because that was my understanding originally), but this way makes much more sense and simplifies my mental model of the world. I no longer have to keep two (not-so) subtly different definitions in my head of what programming-assert means and English-assert means. Now they mean the same thing, which I'm pretty happy about overall.

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

That would be a cool construct as well, don't get me wrong. But considering the vast majority of programs could not reasonably have such proofs, I think the two concepts are orthogonal. I'd rename that to a "prove" statement and not an "assert" because assert has nothing to do with checking and conflating the two has caused confusion.

On 08/02/2014 09:00 AM, Chris Cain wrote:
> On Saturday, 2 August 2014 at 06:36:00 UTC, Timon Gehr wrote:
>>> 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.
>
> Perhaps I just don't understand what you're getting at. It seems
> throughout that you are thinking "statements of fact" has a meaning that
> it's inherently true and is proven or must be proven.
> ...

No, this you made clear already. (However, the post with the explosions was still warranted from my viewpoint, because the terminology was accidentally changed by you and I didn't notice and just implicitly assumed the two expressions were intended to be synonyms.)

> It seems to me that you've suggested:
>
> If falsifiable -> can be proven to be false -> must be proven false ->
> is false
> and
> If verifiable -> can be proven to be true -> must be proven true -> is true
>
> (falsifiable == verifiable)
> (can be proven to be false == can be proven to be true)
> (false == true) is trivially false.
> ...

No, I have suggested that _maybe_

verify != falsify

but that idiomatic usage of

verifiable == falsifiable.

> ...
> If you disagree with my conclusion, I don't
> think there's any more that we can communicate to each other about it. I
> totally understand why you think asserts meant that you wanted the
> compiler to check before (because that was my understanding originally),
> but this way makes much more sense and simplifies my mental model of the
> world. I no longer have to keep two (not-so) subtly different
> definitions in my head of what programming-assert means and
> English-assert means. Now they mean the same thing, which I'm pretty
> happy about overall.
> ...

Indeed, I still disagree with this conclusion, so let's put this aside for now, unless you see another point to discuss. Thanks for having been a reasonable discussion partner.

>> 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.
>
> That would be a cool construct as well, don't get me wrong. But
> considering the vast majority of programs could not reasonably have such
> proofs, I think the two concepts are orthogonal. I'd rename that to a
> "prove" statement and not an "assert" because assert has nothing to do
> with checking and conflating the two has caused confusion.

Well, this was just noting an existing reality that many people with a CS background might have been exposed to.

On Saturday, 2 August 2014 at 07:23:07 UTC, Timon Gehr wrote:
> Thanks for having been a reasonable discussion partner.

Same to you. Have a good evening :)

On Saturday, 2 August 2014 at 06:35:33 UTC, Chris Cain wrote:

> 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

Yes.... I disagreed with you... so yes I am saying something
different. What else is "disagreement" supposed to mean?

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

I understood what you said, I just disagreed with it. Are you
saying I can't disagree???

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

None of these words or phrases are well defined.... if assert was
well defined we would not be talking now....

I understand your argument, I just don't think it is correct.
Particularly I don't agree that your interpretation of assert
more closely matches the real meaning of assert. Let me reiterate
why...

When something is asserted, there is the asserter(the person
making the assertion) and the asserti(s)(the person/people that
are hearing the assertion). Given that any thing that is asserted
can either be true or false, the asserti has no choice but to
conclude that what is being asserted may or may not be true.

In the context of the programmer(asserter) and the
compiler(asserti). The programer is making an assertion that the
compiler must conclude to be either true or false. Because it
does not know if it is true or not, the only time it is
acceptable for the compiler to optimize as if it is true is to
actually check if it is true.

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

The point is that without the check, the assertion is neither
proven or disproven. If the compiler receives bad
input(incorrectly defined input is not bad input), then it knows
it is bad, but the compiler has no way of knowing if an assertion
is good or bad.

If the compiler receives two asserts that can not both be true,
then there is no way it can know what to do, there is no
resolution. But if the compiler is not smart enough to recognize
that they are contradictory then is just compiled an uncompilable
program....

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

I can understand why you think that, I just don't agree. I don't
agree that an assertion in the english language means that
something will be true, I interpret it as a claim that something
may or may not be true.

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


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

That is not an undefined program.... the code you just presented
was completely defined. An an example of an undefined program
with respect to assert is as follows.

assert(x==1);
assert(y==2);


Lets say the compiler was not smart enough to see that these
could not both be true. There is no way the compiler can produce
and thing that is correct because they both cannot be true. There
will always be sets of conditions that the compiler can not prove
to be contradictory(because of the halting problem) but that are.
That is an undefined program...

> The "undefined behavior" is that it allows these two to be equivalent programs.

That is not the undefined behavior

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

That is actually the point, no one would be complaining because
there would be nothing wrong. There would be no chance of
undefined behavior. If the check is always there then the program
will always know that after the assert the condition is true and
would be free to do any optimizations it wants. The undefined
behavior occurs when you optimized as if they are true but do not
check.

On Saturday, 2 August 2014 at 07:36:34 UTC, Tofu Ninja wrote:
> On Saturday, 2 August 2014 at 06:35:33 UTC, Chris Cain wrote:
>
>> 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
>
> Yes.... I disagreed with you... so yes I am saying something
> different. What else is "disagreement" supposed to mean?
>
>> 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.
>
> I understood what you said, I just disagreed with it. Are you
> saying I can't disagree???

It depends on what you mean. You can disagree, but you can't disagree with the fact that what I said and what you seem to suggest I am saying are two different things.

So, in particular,

> So a statement of fact is
> simply the communication that the fact exists.

Is something that seems to be suggesting a meaning in my words that doesn't exist.

Really specifically, I have a problem with "a statement of fact is simply the communication that the fact exists." -> It's a form of communication, but since a fact is defined as "something that is actually the case/exists" and a statement of fact actually isn't communicating that, then it makes a very real difference in the potential interpretation of the words. In particular, your definition of what I'm saying seems to imply that a "statement of fact" suggests that a proof of that fact must exist before an assertion is really an assertion, whereas a real statement of fact doesn't necessarily have a proof of true or false just that it *could be verified.* Thus an assertion without a proof is still an assertion and communicating an idea that doesn't necessarily have to be proven to finalize the communication. It's just that, in particular, the idea communicated is a statement of fact iff it were verifiable. Effectively that definition is just removing extraneous things like beliefs, "god exists", "there exists parallel universes that cease to exist the instant you attempt to observe them", etc. Things that you couldn't verify or falsify.

Basically, because we've had enough problems with what is being actually being said, trying to take some liberties with what is being said and trying to subtly change it is completely out of the question. Until we start coming to an exact understanding of what each other means, it's probably best if we don't disagree with what the other person has defined as what they mean and instead try to figure out what is being said.

If you want to introduce your own definitions and such, make it clear (that is, don't start your paragraph with "I think what you are calling a..." because it's prompting me to carefully consider what you're saying as potentially redefining what I'm saying). It just seemed to me that you were taking my words and trying to suggest that I don't understand my own words or something. If that wasn't what you were trying to do, I'm sorry.

>> 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.
>
> None of these words or phrases are well defined.... if assert was
> well defined we would not be talking now....

That's not necessarily true. Disagreements exist on well-defined definitions all the time.

> I understand your argument, I just don't think it is correct.
> Particularly I don't agree that your interpretation of assert
> more closely matches the real meaning of assert. Let me reiterate
> why...
>
> When something is asserted, there is the asserter(the person
> making the assertion) and the asserti(s)(the person/people that
> are hearing the assertion). Given that any thing that is asserted
> can either be true or false, the asserti has no choice but to
> conclude that what is being asserted may or may not be true.
>
> In the context of the programmer(asserter) and the
> compiler(asserti). The programer is making an assertion that the
> compiler must conclude to be either true or false. Because it
> does not know if it is true or not, the only time it is
> acceptable for the compiler to optimize as if it is true is to
> actually check if it is true.

True, iff the asserter and assertee are human and doubt the assertion. Assertions are typically taken until someone calls into question the assertion. The compiler doesn't call into question anything you do unless it has a proof that what you're doing is wrong.

In particular, I take much of what you say to be truth, even if I haven't explicitly asked you to verify it before we accept it as truth. Furthermore, much of what you say isn't backed up with proof at all (and yet I still accept it without proof). In fact, the vast majority of conversations will do so (otherwise absolutely nothing productive could be accomplished). That said, if I have a reason to believe you are making an incorrect assertion, I will either ask you to verify it or prove you wrong about it. This makes conversations much faster since we often assume things to be true if asserted true by the other party, often skipping checks and verifications that would otherwise potentially be necessary.

Obviously it's starting to sound a lot more like what a compiler does when optimizing a program. When you assert something to the compiler, it accepts it as true unless it has a really good reason to believe it is logically inconsistent (that also suggests that the compiler even tried to make sure it's logically consistent, which I think would be a nice feature to have).

> The point is that without the check, the assertion is neither
> proven or disproven. If the compiler receives bad
> input(incorrectly defined input is not bad input), then it knows
> it is bad, but the compiler has no way of knowing if an assertion
> is good or bad.

I get your point, but I see asserts in the same class as most (all?) other mechanisms. If it does not have a proof against what you say, then it will not step in. You don't have to write proven programs in general.

Since it doesn't have to prove your assertion (and it can't in general, so that's a good thing), then it must accept your assertion as good just like it accepts all of your other code as logically good unless it has a reason to believe that it's not.

> If the compiler receives two asserts that can not both be true,
> then there is no way it can know what to do, there is no
> resolution. But if the compiler is not smart enough to recognize
> that they are contradictory then is just compiled an uncompilable
> program....

I've already covered that I think things that are provably false might be helpful if the compiler actually pointed out the error. That said, it's not a trivial problem to solve, so it's not surprising that it doesn't solve it.

> I can understand why you think that, I just don't agree. I don't
> agree that an assertion in the english language means that
> something will be true, I interpret it as a claim that something
> may or may not be true.

Of course. But what point is there in telling a compiler that? Obviously there's no point unless you're communicating some idea to the compiler and communicating to the compiler that "here's something that may or may not be true, so don't do anything about it" is completely odd, strange, and special (in the sense that there doesn't exist any other construct that I can think of that does that... even ASM noops, which literally mean "do nothing", have a purposeful effect on a program).

I expect a compiler to help me out, but ultimately I expect it to trust my logic even if it can't verify it. Specifically, I don't mind it stepping in with counter proofs to my suggestion that I have a good program. But if it doesn't know whether my program is good or not, I expect it to assume it is good. I've already shown that your expectations for `if` statements and function calls are almost certainly the same as my expectations for all language features.

> That is not an undefined program.... the code you just presented
> was completely defined. An an example of an undefined program
> with respect to assert is as follows.
>
> assert(x==1);
> assert(y==2);
>
>
> Lets say the compiler was not smart enough to see that these
> could not both be true. There is no way the compiler can produce
> and thing that is correct because they both cannot be true. There
> will always be sets of conditions that the compiler can not prove
> to be contradictory(because of the halting problem) but that are.
> That is an undefined program...
>
>> The "undefined behavior" is that it allows these two to be equivalent programs.
>
> That is not the undefined behavior

Fine, I see what you mean. But I don't find it persuasive because I just see it as a bad program no different than one constructed from any other logic error. It'd be nice to have better constructs to help prove correctness, but we can't do it in general.

But in the context of what we actually can do, asserts make sense to behave as described in this thread.

> That is actually the point, no one would be complaining because
> there would be nothing wrong. There would be no chance of
> undefined behavior. If the check is always there then the program
> will always know that after the assert the condition is true and
> would be free to do any optimizations it wants. The undefined
> behavior occurs when you optimized as if they are true but do not
> check.

Actually, there would be something wrong. Two *very* different programs would be compiled between an optimized build with checked assertions and a program without checked assertions.

The difference of the programs with asserts as described in this thread would be precisely the asserts themselves, which is absolutely what you'd expect. No one would expect that removing asserts could completely change *everything* about the code, which is what is concluded by the behavior you describe.

Of course, you could suggest that "asserts shouldn't affect optimization" -> but the problem there is that it matches no definition of the English language version of assert because it means "check to see if this is true" which is very, VERY far away from the definition of "statement of fact forcefully". Hence why I'm very eager to cast off that definition because it has a meaning that is no where near the English definition.

On Saturday, 2 August 2014 at 07:36:34 UTC, Tofu Ninja wrote:
> ...

Look, this is the point I'm trying to make. Given the English definition of assert (Just accept the definition, I'm tired: "statement of fact or belief confidently and forcefully"), I claim that it makes sense that a compiler will use your statement of fact to do something meaningful. The assert defined in this topic by Walter certainly aligns with what *I* would expect the compiler to do, given a statement of fact. Yes, whatever you said may be true or may not be true. Just like anything else, though, if you're wrong, your program will be buggy. Such is life of a programmer.

I find the concept of not doing anything meaningful with an assert to be strange. I find the idea of confusing "checking" with "asserting" to also be pretty weird (only after this topic, to be fair). Given the English definition of assert, it seems strange that I ever believed it should work the way I conceptualized it before. But oh well. That's all I really wanted to say, I'm really tired of words and throwing things around and confusing something so simple and trivial. Simple things should stay simple. Complexity hides incorrect logic.

To simplify: When I tell the compiler to do something, it does it. Thus, if I give a compiler a statement of fact, it should use that information. There should be no special case between those two. Yeah whatever, compile errors, come on man, stop missing the simple and obvious point. Stop missing the forest for the grain of dirt.

On 08/02/14 11:36, Chris Cain via Digitalmars-d wrote:
> On Saturday, 2 August 2014 at 07:36:34 UTC, Tofu Ninja wrote:
>> ...
> 
> Look, this is the point I'm trying to make. Given the English definition of assert

We're not writing code in `English`, but in `D`. That is a fact. :) The english definition of 'assert' is *completely irrelevant*. Really.

artur

On Saturday, 2 August 2014 at 05:07:58 UTC, Chris Cain wrote:
> On Saturday, 2 August 2014 at 04:40:53 UTC, Tofu Ninja wrote:
>> 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?

But he _does_ want the compiler to do something: check whether it's true (or more precisely: check whether it's not false in this particular case). He wants it to be exactly equivalent to:

    version(assert)
    if(!(condition))
        throw new AssertError(...);

Now, you could ask: Why use `assert` instead of writing it like this? Well, for one, it's more concise, and secondly, it shows that your intention is to check the semantic validity of your program, and not just do an arbitrary check that is part of your algorithm.

On Saturday, 2 August 2014 at 05:07:58 UTC, Chris Cain wrote:
> Thus when you assert something is true and the compiler can't immediately disprove you, it must follow what you say.

The compiler can be much better about proving things about a program than programmers probably are, especially if subtle details of the language specification need to be taken into account, because this is mostly a mechanical thing, which computers are really good at, and humans are not. If the compiler cannot prove something, it will usually err on the safe side (let's assume an error free compiler).

I think whole program optimization is a much better strategy. With that, the compiler can actually prove what you just have to assume if you use manual assertions. Of course, it doesn't work across library boundaries, but I would see those as external interfaces, so it's probably acceptable.