From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Spam-Checker-Version: SpamAssassin 3.1.3 (2006-06-01) on yquem.inria.fr X-Spam-Level: X-Spam-Status: No, score=0.0 required=5.0 tests=AWL autolearn=disabled version=3.1.3 X-Original-To: caml-list@yquem.inria.fr Delivered-To: caml-list@yquem.inria.fr Received: from mail3-relais-sop.national.inria.fr (mail3-relais-sop.national.inria.fr [192.134.164.104]) by yquem.inria.fr (Postfix) with ESMTP id BA6E6BC69 for ; Thu, 4 Oct 2007 18:37:25 +0200 (CEST) X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AgAAABOzBEfAXQInemdsb2JhbACOOAEBCQo X-IronPort-AV: E=Sophos;i="4.21,230,1188770400"; d="scan'208";a="3759225" Received: from concorde.inria.fr ([192.93.2.39]) by mail3-smtp-sop.national.inria.fr with ESMTP; 04 Oct 2007 18:37:25 +0200 Received: from mail1-relais-roc.national.inria.fr (mail1-relais-roc.national.inria.fr [192.134.164.82]) by concorde.inria.fr (8.13.6/8.13.6) with ESMTP id l94GbOtZ008420 (version=TLSv1/SSLv3 cipher=RC4-SHA bits=128 verify=OK) for ; Thu, 4 Oct 2007 18:37:25 +0200 X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AgAAABOzBEfLENaMnmdsb2JhbACOOAEBAgcEBic X-IronPort-AV: E=Sophos;i="4.21,230,1188770400"; d="scan'208";a="2143490" Received: from ipmail01.adl2.internode.on.net ([203.16.214.140]) by mail1-smtp-roc.national.inria.fr with ESMTP; 04 Oct 2007 18:37:23 +0200 X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AgAAAG6xBEd5LHvc/2dsb2JhbAAM X-IronPort-AV: E=Sophos;i="4.21,230,1188743400"; d="scan'208";a="204256512" Received: from ppp121-44-123-220.lns10.syd6.internode.on.net (HELO [192.168.1.201]) ([121.44.123.220]) by ipmail01.adl2.internode.on.net with ESMTP; 05 Oct 2007 02:07:22 +0930 Subject: Re: [Caml-list] Unsoundness is essential From: skaller To: Andrej.Bauer@andrej.com Cc: caml-list@inria.fr In-Reply-To: <470506D9.3080704@fmf.uni-lj.si> References: <20071003083529.40DA2A99F@Adric.metnet.fnmoc.navy.mil> <4703FDEF.7030900@univ-savoie.fr> <1191451810.7218.86.camel@rosella.wigram> <1191462724.7542.76.camel@rosella.wigram> <47049A6D.6020201@univ-savoie.fr> <4704AAA8.9080602@lix.polytechnique.fr> <1191509355.6518.104.camel@rosella.wigram> <470506D9.3080704@fmf.uni-lj.si> Content-Type: text/plain Date: Fri, 05 Oct 2007 02:37:21 +1000 Message-Id: <1191515841.6518.185.camel@rosella.wigram> Mime-Version: 1.0 X-Mailer: Evolution 2.10.1 Content-Transfer-Encoding: 7bit X-Miltered: at concorde with ID 470516C5.000 by Joe's j-chkmail (http://j-chkmail . ensmp . fr)! X-Spam: no; 0.00; 0200,:01 andrej:01 forall:01 runtime:01 compiler:01 sourceforge:01 wrote:01 caml-list:01 functions:01 int:01 int:01 let:03 applied:05 thu:05 timeout:05 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 Felix, successor to C++: http://felix.sf.net