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.
