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 mail3-relais-sop.national.inria.fr (mail3-relais-sop.national.inria.fr [192.134.164.104]) by yquem.inria.fr (Postfix) with ESMTP id E77D1BC73 for ; Thu, 4 Oct 2007 17:04:12 +0200 (CEST) X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AgAAAMCdBEfAXQImh2dsb2JhbACOOAEBCQon X-IronPort-AV: E=Sophos;i="4.21,230,1188770400"; d="scan'208";a="3755175" Received: from discorde.inria.fr ([192.93.2.38]) by mail3-smtp-sop.national.inria.fr with ESMTP; 04 Oct 2007 17:04:12 +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 l94F42bQ021132 (version=TLSv1/SSLv3 cipher=RC4-SHA bits=128 verify=OK) for ; Thu, 4 Oct 2007 17:04:12 +0200 X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: Ao8CAMCdBEfBAkMt/2dsb2JhbAA X-IronPort-AV: E=Sophos;i="4.21,230,1188770400"; d="scan'208";a="2139124" Received: from vega.fmf.uni-lj.si (HELO postar.fmf.uni-lj.si) ([193.2.67.45]) by mail1-smtp-roc.national.inria.fr with ESMTP; 04 Oct 2007 17:03:34 +0200 Received: from localhost (unknown [192.168.5.1]) by postar.fmf.uni-lj.si (Postfix) with ESMTP id 25F7718B0E4; Thu, 4 Oct 2007 17:03:34 +0200 (CEST) X-Virus-Scanned: amavisd-new at spam.fmf.uni-lj.si Received: from postar.fmf.uni-lj.si ([192.168.5.5]) by localhost (spam.fmf.uni-lj.si [192.168.5.1]) (amavisd-new, port 10024) with ESMTP id kc8wmtgMgWHx; Thu, 4 Oct 2007 17:03:31 +0200 (CEST) Received: from [193.2.67.88] (unknown [193.2.67.88]) by postar.fmf.uni-lj.si (Postfix) with ESMTP id C8A5E18B0D9; Thu, 4 Oct 2007 17:03:31 +0200 (CEST) Message-ID: <470500F9.1080301@fmf.uni-lj.si> Date: Thu, 04 Oct 2007 17:04:25 +0200 From: Andrej Bauer Reply-To: Andrej.Bauer@andrej.com User-Agent: Thunderbird 1.5.0.13 (X11/20070824) MIME-Version: 1.0 To: caml-list@inria.fr Cc: Arnaud Spiwack 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> In-Reply-To: <4704AAA8.9080602@lix.polytechnique.fr> Content-Type: text/plain; charset=ISO-8859-2; format=flowed Content-Transfer-Encoding: 8bit X-Miltered: at discorde with ID 470500E2.000 by Joe's j-chkmail (http://j-chkmail . ensmp . fr)! X-Spam: no; 0.00; andrej:01 andrej:01 theorems:01 christophe:01 raffalli:01 christophe:01 raffalli:01 theorems:01 decidability:01 well-typed:01 well-typed:01 ocaml:01 ocaml:01 decidable:01 decidability:01 I too have a compulsive obsession to talk about logic, so here is my contribution. Logic is about details. It is only to be expected that in a willy-waving competition on a mailing list like ours everyone will get something wrong about such a tricky thing as Goedel's theorems (me included). For example: Christophe Raffalli: > - 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 ... In logic complete usually means: for every sentence A the system proves A or it proves not A. This has nothing to do with being able to interpret arithmetic. We can define completeness without reference to arithmetic. (Presumably, a type system is complete if for every (closed) type A, A is inhabited or A -> void is inhabited. At least this would be the reading of completeness under propositions-as-types.) Christophe Raffalli: > - The 1st incompleteness theorem states that no theory containing > arithmetic is complete. No _sound_ theory interpreting arithmetic is complete. Arnaud Spiwack wrote: > Anyway, back to Mr. Gödel and his theorem. What he stated indeed is that > truth and provability never coincide (provided we're talking of > something at least as expressive as arithmetic). Goedel's theorems say nothing directly about truth. This is a common misconception. Skaller started the discussion with a rerefence to Geodel, which he did not attempt to use in a technically correct way. I think it would be beneficial for this discussion to move away from explicit references to Goedel. We seem to be talking about two things: a) Expressiveness of a type system vs. decidability of type-checking. The main point is that the more expressive the type system the harder it is to check types. b) Safety guarantees for well-typed programs A typical safety guarantee is expressed with the Preservation Lemma ("Types are preserved during evaluation") and Progress Lemma ("A typed program is either a value or has a next evaluation step"). Together these two imply, e.g., that there won't be a segmentation fault. I think to some extent (b) is what skaller calls "soundness". If I read skaller correctly, he made three points (please correct me if not): 1) The safety properties of well-typed programs in C are none, but Ocaml is not much better either, since it just pretends that exceptions are safe. Therefore, to at least some degree the slogan "the Ocaml type system guarantees safety" is not entirely and honestly true. 2) Morally inferior languages such as C and Python are popular because people are not willing to write programs with their hands tied to their backs by a typing system. 3) Skaller would rather have poor safety guarantees than an inexpressive type system that ties his hands. Goedel is dragged in only because his theorems tell us that the perfect world does not exist, i.e., we cannot have decidable type checking of a very expressive type system which also has sane safety properties. Leaving Goedel aside for a moment, we can ask what a good practical combination of expressiveness and safety would be. We have to give up at least one of the three desired properties (expressiveness, decidability of type checking, safety). Various languages make various choices, as was already mentioned in this thread. Let me just say that the choice made by C, i.e., to give up both expressiveness and safety in return for easy type-checking is not as crazy as it may sound (imagine it's 1970, your computer has 4kb of memory, everybody around you thinks of types as hints to compilers about how many bytes of storage a variable will take, and Martin-Lof is just an obscure Scandinavian mathematician and/or philosopher that real programmers never heard of). It seems to me that the evolution of theory-backed languages such as ML and Haskell is reaching a point where people are willing to give up decidability of type-checking (Haskell has done it). Skaller seems to think that the only option is to give up safety, as well, with which I disagree. We need _controlled_ unsafety. My position is this: i) Insist on good safety properties. If a program compiles without any "ifs" and "buts", then it is safe (whatever that means). It the compiler thinks the program might be unsafe it should try to compile anyhow, and tell us why precisely it thinks it might be unsafe. ii) Give programmers very expressive type systems so that they can write things like div : int * {x : int | not (x = 0)} -> int and much more. iii) Of course, by combining i) and ii) we must then give up decidability of type-checking. We can compensate for that loss by _making compilers more interactive_. The current model, where a compiler either succeeds on its own or fails completely, is not going to take us much further. People from the automated theorem proving community learnt a while ago that the interaction between the human and the computer is the way to go. A compiler should be able to take hints on how to check types. The result of compilation should be one of: - everything is ok - the program contains a grave typing error which prevents the compiler from emitting sane code, compilation is aborted - the compiler generates sane code but also emits a list of assertions which need to be checked (by humans or otherwise) in order to guarantee safety If we had compilers like that, they would greatly encourage good programming practices. You can read the above as my manifesto, if you wish. Best regards, Andrej