checkedint call removal

Fri Aug 1 22:32:42 PDT 2014

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?