Re: [Caml-list] Unsoundness is essential

[skaller <skaller@users.sourceforge.net>]

On Thu, 2007-10-04 at 17:29 +0200, Andrej Bauer wrote:

> It is very easy to come up with preconditions that are computationally 
> unverifiable.
[]
> Or to give you a much more simplistic example:
> 
> fun find_zero (f: int -> int where not (forall n:int, f(n) != 0)) {
>    int i = 0;
>    while (f(i) != 0) { i++; }
>    return i;
> }
> 
> How will you verify the precondition on f at runtime?  In this case I 
> would expect the compiler to list all uses of find_zero applied to 
> functions which are not known not have a zero. Let the human worry.

One 'solution' is a timeout. However I would apply the timeout
to the actual find_zero function, not the pre-condition.

The 'convex' example is better, because the pre-condition is not
so obviously closely coupled to the calculation. Also, the
result of a calculation is likely to be simply *wrong*.

-- 
John Skaller <skaller at users dot sf dot net>
Felix, successor to C++: http://felix.sf.net