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