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 mail4-relais-sop.national.inria.fr (mail4-relais-sop.national.inria.fr [192.134.164.105]) by yquem.inria.fr (Postfix) with ESMTP id 23E99BC69 for ; Thu, 4 Oct 2007 17:28:40 +0200 (CEST) X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AgAAACKjBEfAXQImh2dsb2JhbACOOAEBCQon X-IronPort-AV: E=Sophos;i="4.21,230,1188770400"; d="scan'208";a="17296651" Received: from discorde.inria.fr ([192.93.2.38]) by mail4-smtp-sop.national.inria.fr with ESMTP; 04 Oct 2007 17:28:39 +0200 Received: from mail2-relais-roc.national.inria.fr (mail2-relais-roc.national.inria.fr [192.134.164.83]) by discorde.inria.fr (8.13.6/8.13.6) with ESMTP id l94FSdFQ023313 (version=TLSv1/SSLv3 cipher=RC4-SHA bits=128 verify=OK) for ; Thu, 4 Oct 2007 17:28:39 +0200 X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: Ao8CAGSjBEfBAkMt/2dsb2JhbAA X-IronPort-AV: E=Sophos;i="4.21,230,1188770400"; d="scan'208";a="2381766" Received: from vega.fmf.uni-lj.si (HELO postar.fmf.uni-lj.si) ([193.2.67.45]) by mail2-smtp-roc.national.inria.fr with ESMTP; 04 Oct 2007 17:28:38 +0200 Received: from localhost (unknown [192.168.5.1]) by postar.fmf.uni-lj.si (Postfix) with ESMTP id 8D62812A954; Thu, 4 Oct 2007 17:28:38 +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 nMLh-4fBcEtb; Thu, 4 Oct 2007 17:28:36 +0200 (CEST) Received: from [193.2.67.88] (unknown [193.2.67.88]) by postar.fmf.uni-lj.si (Postfix) with ESMTP id E58A118B1E3; Thu, 4 Oct 2007 17:28:35 +0200 (CEST) Message-ID: <470506D9.3080704@fmf.uni-lj.si> Date: Thu, 04 Oct 2007 17:29:29 +0200 From: Andrej Bauer Reply-To: Andrej.Bauer@andrej.com 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> <47049A6D.6020201@univ-savoie.fr> <4704AAA8.9080602@lix.polytechnique.fr> <1191509355.6518.104.camel@rosella.wigram> In-Reply-To: <1191509355.6518.104.camel@rosella.wigram> Content-Type: text/plain; charset=ISO-8859-2; format=flowed Content-Transfer-Encoding: 7bit X-Miltered: at discorde with ID 470506A7.000 by Joe's j-chkmail (http://j-chkmail . ensmp . fr)! X-Spam: no; 0.00; andrej:01 andrej:01 compiler:01 compilation:01 compiler:01 runtime:01 runtime:01 forall:01 assertions:01 typechecking:01 caml-list:01 functions:01 minor:01 expressive:01 int:01 At the danger of repeating myself (for which I apologize), I would like to convince skaller that he does not want unsound type systems. (What skaller calls "sound" I call "safety property" in my previous post.) Skaller, you want something like this: (a) expressive power (dependent types, subsets, you-name-it) (b) soundness, in the following form: * the compiler rejects obvious nonsense * the result of a compilation is a program and a list of assertions which the compiler was unable to verify This I would call "controlled unsoundness" which at least allows the human to see what needs to be verified to guarantee soundness. It's much better than the sort of unsoundness that skaller seems to be advocating. There is actually a new minor point I want to make: you cannot postpone all problems with typechecking to runtime. Only very simple conditions, such as bounds checks, can be checked at runtime. It is very easy to come up with preconditions that are computationally unverifiable. For example, you might have a numerical method for zero-finding which only works if the input is a function satisfying a funky condition, e.g., "the function is convex". How are you going to check that at runtime? 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. Andrej