English version
Accueil     Ŕ propos     Téléchargement     Ressources     Contactez-nous    

Ce site est rarement mis ŕ jour. Pour les informations les plus récentes, rendez-vous sur le nouveau site OCaml ŕ l'adresse ocaml.org.

Browse thread
Locally-polymorphic exceptions [was: folding over a file]
[ Home ] [ Index: by date | by threads ]
[ Search: ]

[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
Date: 2007-10-04 (16:37)
From: skaller <skaller@u...>
Subject: Re: [Caml-list] Unsoundness is essential
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