Decorated intervals ARE intervals...
Dan Zuras (and before that, Nate Hayes) quoted Dominique Lohez:
> Even a cautious programmer may fail.
>
> Thus the program must never lie
> It must never believe the programmer implicit extra-assertions
> and check from known data and decorations
I have to disagree. Crutches to help a less-than-perfect programmer
are useful, but we should not outlaw rock climbing!
There must be a way for a knowledgeable programmer to communicate
to the compiler or run-time knowledge that cannot be derived by the
compiler. Such assertions must of course be explicit, so that they
can be checked by an independent equally-qualified programmer. We
know that the problem of proving correctness is in general undecidable
or untractable, except by severely crippling the expressiveness of the
language (e.g. loop-free, or counted loops only, with no external
function invocations). The best be can do is local correctness, given
additional assertions which must be believed (though incorrect assertions
can frequently be detected and cause abnormal termination, as an extra
level of protection).
Revising decorations that are KNOWN by the programmer to be overly
pessimistic must be possible, if the program is expected to be useful.
Otherwise we could simply mandate that every program return "Entire;
something may or may not have gone wrong". That would indeed never lie!
The trouble we are facing is that there are no standard ways to do
the necessary assertions. We should try to address that issue -- and
explicit control of decorations, as well as declarations of dependence
or independence, are some of the possible mechanisms.
Related to this issue is case-by-case definitions, e.g. Dan Zuras'
potential well problem that led to Dominique's statement. The final
result is the union of two distinct paths. Now, with interval arguments
the choice of which path would be taken by any particular point value
is perhaps uncertain (which is why both paths are computed), but in fact
only one path actually contributes to the result, and what could have
happened on the other path, for values that are indeed outside of the
assumptions on which that path relies, should NOT pollute the final
result. After all, the whole point of splitting the computation is to
satisfy the assumptions!
Now, it is true that not every case decomposition has this property, and
should we get compilers that can tell the good and bad cases apart, we
could perhaps handle the decoration merging automatically. But I'm afraid
Mr. Turing spoiled that possibility -- and that's why we need to allow the
programmer to assert the necessary conditions.
Michel.
---Sent: 2011-07-02 18:29:57 UTC