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 mail4-relais-sop.national.inria.fr (mail4-relais-sop.national.inria.fr [192.134.164.105]) by yquem.inria.fr (Postfix) with ESMTP id EAC15BC69 for ; Thu, 4 Oct 2007 18:25:24 +0200 (CEST) X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AgAAADKxBEfAXQImh2dsb2JhbACOOAEBCQon X-IronPort-AV: E=Sophos;i="4.21,230,1188770400"; d="scan'208";a="17299111" Received: from discorde.inria.fr ([192.93.2.38]) by mail4-smtp-sop.national.inria.fr with ESMTP; 04 Oct 2007 18:25:24 +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 l94GPOTY028645 (version=TLSv1/SSLv3 cipher=RC4-SHA bits=128 verify=OK) for ; Thu, 4 Oct 2007 18:25:24 +0200 X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AgAAALuwBEfLENaMnmdsb2JhbACOOAEBAgcEBic X-IronPort-AV: E=Sophos;i="4.21,230,1188770400"; d="scan'208";a="2142968" Received: from ipmail01.adl2.internode.on.net ([203.16.214.140]) by mail1-smtp-roc.national.inria.fr with ESMTP; 04 Oct 2007 18:25:22 +0200 X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AgAAAOutBEd5LHvc/2dsb2JhbAAM X-IronPort-AV: E=Sophos;i="4.21,230,1188743400"; d="scan'208";a="204251375" 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 01:55:21 +0930 Subject: Re: [Caml-list] Unsoundness is essential From: skaller To: Andrej.Bauer@andrej.com Cc: caml-list@inria.fr In-Reply-To: <470506D9.3080704@fmf.uni-lj.si> 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> Content-Type: text/plain Date: Fri, 05 Oct 2007 02:25:20 +1000 Message-Id: <1191515120.6518.173.camel@rosella.wigram> Mime-Version: 1.0 X-Mailer: Evolution 2.10.1 Content-Transfer-Encoding: 7bit X-Miltered: at discorde with ID 470513F4.000 by Joe's j-chkmail (http://j-chkmail . ensmp . fr)! X-Spam: no; 0.00; 0200,:01 andrej:01 compiler:01 compilation:01 compiler:01 ocaml:01 ocaml:01 bike:98 sourceforge:01 assertions:01 assertions:01 wrote:01 typing:01 caml-list:01 expressive:01 On Thu, 2007-10-04 at 17:29 +0200, Andrej Bauer wrote: > 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 Yes, I want something like that. > This I would call "controlled unsoundness" As an (eX) motorcyclist I can agree .. riding a bike is like having one continuous controlled road accident.. :) > 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. Sure, but my point does remain: the expressiveness is more or less paramount. It is not so much that I personally desire it or not, but that real programmers in the real world go out there and do whatever is necessary to make programs work. If you can produce a compiler with an expressive type system but cannot yet create a complete list of unproven assertions, that is still better than writing Python. In fact I write a lot of Python even now. I do not do so in ignorance of the value of static type checking! There is a good reason I choose it, for example for the Felix build system. It is not because I fear writing all the types Ocaml would require, but because the need for 'dynamic typing' in this kind of software and the lack of expressiveness in Ocaml type system makes Ocaml unsuitable. Please note I'm *trying* to explain the reason, but probably haven't got it right. The point is, in the manifesto it should go like: expressiveness first, then generating proof obligations, and also with time, improving the automatic provers. The key thing is not to restrict expressiveness just because the type system cannot fully cope.. making the typing more expressive has many benefits by itself. A stupid one: how can theoreticians test the efficacy of a new algorithm with real world case data? -- John Skaller Felix, successor to C++: http://felix.sf.net