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=none autolearn=disabled version=3.1.3 X-Original-To: caml-list@yquem.inria.fr Delivered-To: caml-list@yquem.inria.fr Received: from mail1-relais-roc.national.inria.fr (mail1-relais-roc.national.inria.fr [192.134.164.82]) by yquem.inria.fr (Postfix) with ESMTP id E306BBC69 for ; Thu, 4 Oct 2007 20:59:50 +0200 (CEST) X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AgAAACrVBEfAXQImh2dsb2JhbACOOAEBCQon X-IronPort-AV: E=Sophos;i="4.21,231,1188770400"; d="asc'?vcf'?scan'208";a="2149113" Received: from discorde.inria.fr ([192.93.2.38]) by mail1-smtp-roc.national.inria.fr with ESMTP; 04 Oct 2007 20:59:50 +0200 Received: from mail4-relais-sop.national.inria.fr (mail4-relais-sop.national.inria.fr [192.134.164.105]) by discorde.inria.fr (8.13.6/8.13.6) with ESMTP id l94IxoS6007731 (version=TLSv1/SSLv3 cipher=RC4-SHA bits=128 verify=OK) for ; Thu, 4 Oct 2007 20:59:50 +0200 X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AgAAAB/UBEfUGyodimdsb2JhbACOOAEBCQQGIAc X-IronPort-AV: E=Sophos;i="4.21,231,1188770400"; d="asc'?vcf'?scan'208";a="17304486" Received: from smtp3-g19.free.fr ([212.27.42.29]) by mail4-smtp-sop.national.inria.fr with ESMTP; 04 Oct 2007 20:59:50 +0200 Received: from smtp3-g19.free.fr (localhost.localdomain [127.0.0.1]) by smtp3-g19.free.fr (Postfix) with ESMTP id 5F1E417B557; Thu, 4 Oct 2007 20:59:49 +0200 (CEST) Received: from Tocksi.local (unknown [82.253.223.12]) by smtp3-g19.free.fr (Postfix) with ESMTP id CED9B17B532; Thu, 4 Oct 2007 20:59:48 +0200 (CEST) Message-ID: <47053824.9020701@univ-savoie.fr> Date: Thu, 04 Oct 2007 20:59:48 +0200 From: Christophe Raffalli User-Agent: Thunderbird 2.0.0.6 (Macintosh/20070728) MIME-Version: 1.0 To: skaller Cc: Andrej.Bauer@andrej.com, caml-list@inria.fr Subject: Re: [Caml-list] Unsoundness is essential 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> <1191515841.6518.185.camel@rosella.wigram> In-Reply-To: <1191515841.6518.185.camel@rosella.wigram> X-Enigmail-Version: 0.95.3 Content-Type: multipart/signed; micalg=pgp-sha1; protocol="application/pgp-signature"; boundary="------------enig7B7AC390739127F8EE96C1E7" X-Miltered: at discorde with ID 47053826.000 by Joe's j-chkmail (http://j-chkmail . ensmp . fr)! X-Spam: no; 0.00; christophe:01 raffalli:01 christophe:01 raffalli:01 univ-savoie:01 0200,:01 andrej:01 forall:01 runtime:01 compiler:01 chablais:01 73376:01 univ-savoie:01 wrote:01 lama:01 X-Attachments: cset="utf-8" name="Christophe.Raffalli.vcf" name="Christophe.Raffalli.vcf" type="application/pgp-signature" name="signature.asc" name="signature.asc" This is an OpenPGP/MIME signed message (RFC 2440 and 3156) --------------enig7B7AC390739127F8EE96C1E7 Content-Type: multipart/mixed; boundary="------------060008040802020005040600" This is a multi-part message in MIME format. --------------060008040802020005040600 Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: quoted-printable > On Thu, 2007-10-04 at 17:29 +0200, Andrej Bauer wrote: > > =20 >> It is very easy to come up with preconditions that are computationally= =20 >> unverifiable. >> =20 > [] > =20 >> Or to give you a much more simplistic example: >> >> fun find_zero (f: int -> int where not (forall n:int, f(n) !=3D 0)) { >> int i =3D 0; >> while (f(i) !=3D 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=20 >> functions which are not known not have a zero. Let the human worry. >> =20 > > =20 What's the problem ? If you program with the above function and apply it to a function f, this means you know f will reach zero (otherwise your program will loop). But if you know it, this should mean that you can prove it from the definition of f ? So the only reason to have today programming language that gives not enough safety is because the cost of the formal proof is still to big (by cost, I mean cost to write proof, but also the cost of learning how to write proof ...) --=20 Christophe Raffalli Universite de Savoie Batiment Le Chablais, bureau 21 73376 Le Bourget-du-Lac Cedex tel: (33) 4 79 75 81 03 fax: (33) 4 79 75 87 42 mail: Christophe.Raffalli@univ-savoie.fr www: http://www.lama.univ-savoie.fr/~RAFFALLI --------------------------------------------- IMPORTANT: this mail is signed using PGP/MIME At least Enigmail/Mozilla, mutt or evolution=20 can check this signature. The public key is stored on www.keyserver.net --------------------------------------------- --------------060008040802020005040600 Content-Type: text/x-vcard; charset=utf-8; name="Christophe.Raffalli.vcf" Content-Transfer-Encoding: quoted-printable Content-Disposition: attachment; filename="Christophe.Raffalli.vcf" begin:vcard fn:Christophe Raffalli n:Raffalli;Christophe org:LAMA (UMR 5127) email;internet:christophe.raffalli@univ-savoie.fr title;quoted-printable:Ma=3DC3=3DAEtre de conf=3DC3=3DA9rences tel;work:+33 4 79 75 81 03 note:http://www.lama.univ-savoie.fr/~raffalli x-mozilla-html:TRUE version:2.1 end:vcard --------------060008040802020005040600-- --------------enig7B7AC390739127F8EE96C1E7 Content-Type: application/pgp-signature; name="signature.asc" Content-Description: OpenPGP digital signature Content-Disposition: attachment; filename="signature.asc" -----BEGIN PGP SIGNATURE----- Version: GnuPG v1.4.7 (Darwin) Comment: Using GnuPG with Mozilla - http://enigmail.mozdev.org iD8DBQFHBTgki9jr/RgYAS4RAvnwAJ9Xq8MQt3z392i5ZuwNP9aQ2JSLnACglrsB jLTL8Lz5hBRpMyRP/MW4sKM= =k9Ue -----END PGP SIGNATURE----- --------------enig7B7AC390739127F8EE96C1E7--