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.1 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 mail4-relais-sop.national.inria.fr (mail4-relais-sop.national.inria.fr [192.134.164.105]) by yquem.inria.fr (Postfix) with ESMTP id BCBD6BC69 for ; Thu, 4 Oct 2007 09:47:50 +0200 (CEST) X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AgAAAFM3BEfAXQImh2dsb2JhbACOOAEBCQon X-IronPort-AV: E=Sophos;i="4.21,228,1188770400"; d="asc'?scan'208";a="17273463" Received: from discorde.inria.fr ([192.93.2.38]) by mail4-smtp-sop.national.inria.fr with ESMTP; 04 Oct 2007 09:47:50 +0200 Received: from mail1-relais-roc.national.inria.fr (mail1-relais-roc.national.inria.fr [192.134.164.82]) by discorde.inria.fr (8.13.6/8.13.6) with ESMTP id l947ljA6012483 (version=TLSv1/SSLv3 cipher=RC4-SHA bits=128 verify=OK) for ; Thu, 4 Oct 2007 09:47:50 +0200 X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AgAAAPg2BEfBMHhLh2dsb2JhbACOOAEBCQon X-IronPort-AV: E=Sophos;i="4.21,228,1188770400"; d="asc'?scan'208";a="2114973" Received: from net.univ-savoie.fr ([193.48.120.75]) by mail1-smtp-roc.national.inria.fr with ESMTP; 04 Oct 2007 09:47:49 +0200 Received: from post.bourget.univ-savoie.fr (post.bourget.univ-savoie.fr [193.48.120.73]) by net.univ-savoie.fr (8.12.3/jtpda-5.4) with ESMTP id l947liwr025593 ; Thu, 4 Oct 2007 09:47:44 +0200 Received: from [193.48.123.45] (d45.lama.univ-savoie.fr [193.48.123.45]) by post.bourget.univ-savoie.fr (8.12.3/jtpda-5.4) with ESMTP id l947ktGh008017 ; Thu, 4 Oct 2007 09:46:55 +0200 Message-ID: <47049A6D.6020201@univ-savoie.fr> Date: Thu, 04 Oct 2007 09:46:53 +0200 From: Christophe Raffalli User-Agent: Thunderbird 1.5.0.13 (X11/20070824) MIME-Version: 1.0 To: skaller Cc: 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> In-Reply-To: <1191462724.7542.76.camel@rosella.wigram> X-Enigmail-Version: 0.94.2.0 Content-Type: multipart/signed; micalg=pgp-sha1; protocol="application/pgp-signature"; boundary="------------enigA16EC00DCCA4B63378EA05AD" X-Scanned-By: MIMEDefang 2.33 (www . roaringpenguin . com / mimedefang) X-Miltered: at discorde with ID 47049AA1.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 lacks:01 simulate:01 bug:01 chablais:01 73376:01 univ-savoie:01 sourceforge:01 wrote:01 lama:01 integer:01 X-Attachments: type="application/pgp-signature" name="signature.asc" name="signature.asc" This is an OpenPGP/MIME signed message (RFC 2440 and 3156) --------------enigA16EC00DCCA4B63378EA05AD Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: quoted-printable skaller a =E9crit : > On Wed, 2007-10-03 at 19:28 -0400, Joshua D. Guttman wrote: >> skaller writes: >> >>> Goedel's theorem says that any type system strong enough >>> to describe integer programming is necessarily unsound. >=20 > I paraphrased it, deliberately, in effect claiming an analogous > situation holds with type systems. >=20 Not unsound, incomplete ! you mixup first and second incompleteness theorem. Let's clarify ? - first if a type system does not contain arithmetic nothing can be said (this implies ML), but in this case, the meaning of complete needs to be = clarified. Indeed, there are complete type system ... - The 1st incompleteness theorem states that no theory containing arithmetic is complete. This means that there will always be correct prog= rams that your type system can not accept. However, I thing a real program tha= t is not provably correct in lets say ZF, does not exists and should be rej= ected. you do not accept a program whose correctness is a conjecture (do you ?) - The second incompleteness theorem, states that a system that proves its= own consistency is in fact inconsistent. For type system (strong enough to ex= press arithmetic, like ML with dependant type, PVS, the future PML, ..). This m= eans that the proof that the system is consistent (the proof that "0 =3D 1 can= not be proved") can not be done inside the system. However, the proof that your implement= ation does implement the formal system correctly can be done inside the system,= and this is quite enough for me. - The soundness theorem for ML can be stated as a program of type "int" w= ill - diverge - raise an exception - or produce an int I think everybody except LISP programmers ;-) want a sound type system li= ke this. OK replace everybody by I if you prefer ... For PML, we are more precise = : exception and the fact the a program may diverge must be written in the type. - ML type system is sometimes too incomplete, this is why the Obj library= is here. However, the use of Obj is mainly here because ML lacks dependant types. = In fact, the main use of Obj is to simulate a map table associating to a key k a t= ype t(k) and a value v:t(k). - All this says that a type-system only accepting proved programs is poss= ible and a good idea (it already exists). The question for researcher is how to pr= oduce a type system where the cost of proving is acceptable compared to the cost = of debugging, and this stars to be the case for some specific application, but we are f= ar from having to remove the word "bug" from our vocabulary ;-) --=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 can check this signature. The public key is stored on www.keyserver.net --------------------------------------------- --------------enigA16EC00DCCA4B63378EA05AD 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.6 (GNU/Linux) Comment: Using GnuPG with Mozilla - http://enigmail.mozdev.org iD8DBQFHBJpyi9jr/RgYAS4RAtO/AKDJIb7CAeSi4dLQK3M8CGPAiZHtKwCgrH7y rXj0RLiycqwO/IE30aKtp0c= =ERbG -----END PGP SIGNATURE----- --------------enigA16EC00DCCA4B63378EA05AD--