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.