On 08/02/2014 06:46 AM, Chris Cain wrote:
On Saturday, 2 August 2014 at 04:28:33 UTC, Timon Gehr wrote:
On 08/02/2014 06:11 AM, Chris Cain wrote:
On Saturday, 2 August 2014 at 03:40:47 UTC, Timon Gehr wrote:
I already googled 'statement of fact' myself earlier, and found the
wikipedia entry for 'fact', that I quoted back then:
http://en.wikipedia.org/wiki/Fact
"The usual test for a statement of fact is verifiability, that is,
whether it can be demonstrated to correspond to experience."
I.e. in order to determine whether something is a statement of fact,
one should verify it. Do you agree that it is saying this?
I'll just do this real quick, because it's a really easy one to show the
problem with.
Google "verifiable" ->
http://www.merriam-webster.com/dictionary/verifiable -> "capable of
being verified"
...
Great, now we are getting somewhere.
http://dictionary.reference.com/browse/verify?s=t
"to prove the truth of, as by evidence or testimony; confirm;
substantiate: Events verified his prediction."
I understand "capable of being verified" as "there is a way to verify
this" which is the same as "this can be proven" which would imply
"this is true".
What's wrong here?
The fact that you assume that something "can be proven" means it "has
been proven" or "must be proven". Because you don't necessarily have to
prove it, it doesn't necessarily mean it is true. It's a statement that
you are suggesting is true but *could* be falsified/shown to be
false/verified/verified to be false.
The mere fact that asserts take in expressions show that something "can
be proven", but there is no implication that it, therefore, must be
proven. If you put an expression in an assert and it successfully
compiles, you've made a statement of fact. It's useful that it is
checked/proven in debug builds but not surprising that it's required to
by definition.
...
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?
That is, it's something that has some ability to be verified. Thus, 1==2
is "verifiable" (it can be shown to be either true or false).
...
If I can verify 1==2, I would prove 1==2, as per the definition above,
no?
No.
The definition above was:
"to prove the truth of, as by evidence or testimony; confirm;
substantiate: Events verified his prediction."
You can verify it but find it to be false. Your proof would show it
to be false. The fact that you can write a proof showing it to be false
is a proof that it was verifiable in the first place.
It is possible that this is indeed what it tries to communicate.
Thanks for bearing with me in any case!
No problem. :)
But as I wrote in my previous post, now this brings up the issue that
if an assertion is a statement of fact, then it is not necessarily true.
Why is it now obvious that it should be considered true?
For the same reason that all of the other things you type into a program
is accepted by a program.
...
I see.
`if(...)` ... would it be strange if your program doubted that you
really want to execute the block the if statement refers to? Of course
it would.
Basically, you're a god and what you say to do is law in computer
programming.
(Except if you do something that's 'invalid', at which point all your
carefully crafted laws get ignored immediately.)
By default you expect the computer to not doubt you and to
follow what you say. It's not like a person who will question your
assertions and ask you to prove them or double check them for you.
...
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.
Though, the fact that it will double check them for you is helpful in
debug builds, so it's an obvious enhancement for debugging purposes.
Since assert is you making a statement of fact,
Note that it might just as well be a command that makes the program make
a statement of fact.
it's logical that it
should, by default, accept what you say just like it accepts every other
command you give it.
...
Yes, but what I say is: "I assert this." And _I_ do. If I do just this,
this does not determine what _the compiler_ is to make of it. We need a
separate operational semantics which IMO is not obvious a priori given
just the definition in English and knowledge about programming without
anything concerning 'assert'.
If you're wrong... well, it's just like if you're wrong about your if
statements or if you call the wrong function or pass in the wrong
variables.
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.
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?
