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.
