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 mail2-relais-roc.national.inria.fr (mail2-relais-roc.national.inria.fr [192.134.164.83]) by yquem.inria.fr (Postfix) with ESMTP id 14C1EBC69 for ; Thu, 4 Oct 2007 17:07:41 +0200 (CEST) X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AgAAAC6eBEfAXQInemdsb2JhbACOOAEBCQo X-IronPort-AV: E=Sophos;i="4.21,230,1188770400"; d="scan'208";a="2380849" Received: from concorde.inria.fr ([192.93.2.39]) by mail2-smtp-roc.national.inria.fr with ESMTP; 04 Oct 2007 17:07:40 +0200 Received: from mail4-relais-sop.national.inria.fr (mail4-relais-sop.national.inria.fr [192.134.164.105]) by concorde.inria.fr (8.13.6/8.13.6) with ESMTP id l94F7ZI8032642 (version=TLSv1/SSLv3 cipher=RC4-SHA bits=128 verify=OK) for ; Thu, 4 Oct 2007 17:07:40 +0200 X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AgAAAC6eBEfLENaMnmdsb2JhbACOOAEBAgcEBic X-IronPort-AV: E=Sophos;i="4.21,230,1188770400"; d="scan'208";a="17295756" Received: from ipmail01.adl2.internode.on.net ([203.16.214.140]) by mail4-smtp-sop.national.inria.fr with ESMTP; 04 Oct 2007 17:07:39 +0200 X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AgAAAJOcBEd5LHvc/2dsb2JhbAAM X-IronPort-AV: E=Sophos;i="4.21,230,1188743400"; d="scan'208";a="204218857" 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 00:37:36 +0930 Subject: Re: [Caml-list] Unsoundness is essential From: skaller To: Vincent Hanquez Cc: David Allsopp , caml-list@inria.fr In-Reply-To: <20071004124549.GA24788@snarc.org> References: <1191461066.7542.48.camel@rosella.wigram> <018201c80679$86a2ba00$017ca8c0@countertenor> <20071004124549.GA24788@snarc.org> Content-Type: text/plain Date: Fri, 05 Oct 2007 01:07:35 +1000 Message-Id: <1191510455.6518.118.camel@rosella.wigram> Mime-Version: 1.0 X-Mailer: Evolution 2.10.1 Content-Transfer-Encoding: 7bit X-Miltered: at concorde with ID 470501B7.000 by Joe's j-chkmail (http://j-chkmail . ensmp . fr)! X-Spam: no; 0.00; 0200,:01 0100,:01 ocaml:01 bindings:01 ocaml:01 bug:01 ill-typed:01 annotations:01 worn:98 prison:98 sourceforge:01 wrote:01 wrote:01 abstract:01 compile:01 On Thu, 2007-10-04 at 14:45 +0200, Vincent Hanquez wrote: > On Thu, Oct 04, 2007 at 12:26:53PM +0100, David Allsopp wrote: > > Personally, whenever I go back to C, the novelty of the relaxed type > > system is instantly worn away on the first tricky-to-repeat core dump... at > > least an Ocaml exception has a cat in hell's chance of being found > > systematically! > > That's sadly not true. GC bugs in some bindings are usually hard to find ! I think David's point is that many faults in C are diagnosed, if at all, by a very hard to analyse output (a core dump). Whereas in Ocaml more bugs are caught at compile time, and, often a bug at run time has some simple abstract information such as an exception constructor name, which help in pinpointing the problem. I don't think the claim was *elimination* as much as *improvement*. However I thin David is missing my argument if he's thinking I am arguing for a more relaxed type system: on the contrary I want an even tighter type system. The problem is that the cost is likely to be unsoundness -- in the process of making the type system more expressive, we're bound to be forced to let some ill-typed programs through because it is no longer feasible to prove well-typedness in all cases. My argument is that this just isn't a problem to worry about: the only difference is that existing buggy programs which were previously judged type correct, are no longer decided as type correct. In some cases a program will be let through by BOTH type systems, and in others the more expressive system will find the error, so the fact that the type system is unsound is not a problem: our confidence in the correctness of the program is *enhanced* despite the unsoundness. Furthermore, my program which today is accepted may be rejected tomorrow when a theorist finds some way to reduce the unsoundness by catching more cases. This is impossible if you don't let me write the annotations just because you can't prove the well typedness right now! BTW: when I say 'type system' and 'soundness' I mean *static type checking*. I do not consider dynamic typing as a type system in this sense. Any type test at run time is instant proof of unsoundness of the type system: an ill typed program has been allowed to escape to run time. The fact that a policeman is set to catch the inmate who escaped from jail does not in any way diminish the fact the inmate indeed escaped, and the jail security system was unsound (Ouch .. new season of Prison Break .. :) -- John Skaller Felix, successor to C++: http://felix.sf.net