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 02F3EBC69 for ; Thu, 4 Oct 2007 18:04:00 +0200 (CEST) X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AgAAAJOrBEfLENaMnmdsb2JhbACOOAEBAgcEBic X-IronPort-AV: E=Sophos;i="4.21,230,1188770400"; d="scan'208";a="2383040" Received: from concorde.inria.fr ([192.93.2.39]) by mail2-smtp-roc.national.inria.fr with ESMTP; 04 Oct 2007 18:03:59 +0200 Received: from mail2-relais-roc.national.inria.fr (mail2-relais-roc.national.inria.fr [192.134.164.83]) by concorde.inria.fr (8.13.6/8.13.6) with ESMTP id l94G3xYm005075 (version=TLSv1/SSLv3 cipher=RC4-SHA bits=128 verify=OK) for ; Thu, 4 Oct 2007 18:03:59 +0200 X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AgAAAJOrBEfLENaMnmdsb2JhbACOOAEBAgcEBic X-IronPort-AV: E=Sophos;i="4.21,230,1188770400"; d="scan'208";a="2383039" Received: from ipmail01.adl2.internode.on.net ([203.16.214.140]) by mail2-smtp-roc.national.inria.fr with ESMTP; 04 Oct 2007 18:03:57 +0200 X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AgAAAO+pBEd5LHvc/2dsb2JhbAAM X-IronPort-AV: E=Sophos;i="4.21,230,1188743400"; d="scan'208";a="204242226" 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:33:55 +0930 Subject: Re: [Caml-list] Unsoundness is essential From: skaller To: Andrej.Bauer@andrej.com Cc: caml-list@inria.fr In-Reply-To: <470500F9.1080301@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> <470500F9.1080301@fmf.uni-lj.si> Content-Type: text/plain Date: Fri, 05 Oct 2007 02:03:54 +1000 Message-Id: <1191513834.6518.156.camel@rosella.wigram> Mime-Version: 1.0 X-Mailer: Evolution 2.10.1 Content-Transfer-Encoding: 7bit X-Miltered: at concorde with ID 47050EEF.000 by Joe's j-chkmail (http://j-chkmail . ensmp . fr)! X-Spam: no; 0.00; 0200,:01 andrej:01 invariants:01 symmetric:01 typeclass:01 inv:01 inv:01 typeclass:01 haskell:01 axioms:01 semantics:01 axioms:01 associative:01 notation:01 compiler:01 On Thu, 2007-10-04 at 17:04 +0200, Andrej Bauer wrote: [] Thanks. I think this is a very good interpretation of my intent. > 3) Skaller would rather have poor safety guarantees than an inexpressive > type system that ties his hands. That's not quite right: it isn't that typing prevents me writing my programs (it does sometimes, but usually that indicates a design fault). It's more like the lack of expressiveness prevents me writing down the invariants and so forth I actually want to. I have to keep them in my head, or write them as comments where they're not sanity checked. In Felix for example the standard library contains this: // additive symmetric group typeclass FloatAddgrp[t] { inherit Eq[t]; virtual fun zero: 1 -> t; virtual fun add: t * t -> t; virtual fun neg: t -> t; virtual fun sub(x:t,y:t):t => add (x,neg y); reduce id (x:t): x+zero() => x; reduce id (x:t): zero()+x => x; reduce inv(x:t): x-x => zero(); reduce inv(x:t): - (-x) => x; axiom sym (x:t,y:t): x+y == y+x; } typeclass Addgrp[t] { inherit FloatAddgrp[t]; axiom assoc (x:t,y:t,z:t): (x+y)+z == x+(y+z); reduce inv(x:t,y:t): x+y-y => x; } and here I can encode a LOT more information about the type T the typeclass describes than Haskell allows. Furthermore, the 'reduce' axioms have operational semantics (Felix really does apply these reductions) and the axioms can be tested by using a statement like check(1,2); which is how I discovered floating point arithmetic isn't associative -- an actual regression test failed. What is more Felix allows a 'lemma' which is an axiom which is made into a proof goal in Why format for submission to a theorem prover. This notation is weak, and the Felix compiler cannot really prove much with it: for example it does not check instances of typeclasses meet their obligations. But at least the semantics are encoded in the language and type checked, I can make reasoned arguments based on the stated semantics, and there is some hope someone will come along and implement some actual proof procedures and/or optimisations at a later date. [I really have proven one trivial lemma using both Ergo and Simplify.] Vincent Aravantinos made the important point: "If you allow everything (such as the "type expressive" C you are envisaging), the programmer will be tempted to use this "everything" whereas he could achieve the same with a "bounded" language." and the admission of semantics into the system is the starting point for allowing one to at least state some of those bounds (even if there is little or no enforcement the bounds are formalised). > 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. Ooops, I am sprung! > Skaller seems to > think that the only option is to give up safety, as well, with which I > disagree. We need _controlled_ unsafety. Actually I HOPED someone smart enough would dare make such a proposal. I think I alluded to this idea in the claims that adding unsound typing to the existing Ocaml type system such as non-zero integers will not actually compromise safety, but rather enhance it. However I just do not understand how to say 'It is safe up to this point, and risky from there on'. I have no mental concept of 'delimited unsoundness'. In an analogous context I had no idea how to mix side-effecting and functional code in a delimited way until I saw how Haskell does it with Monads. > 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. Of course, all pragmatic compilers offer switches to control this kind of thing. > 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. Ah. > 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. This is quite good from an industrial viewpoint. The list of assertions can be reduced by more work in selective areas as a complement to testing. This gives managers control over risk. It seems a consequence of this manifesto is that the asserting of the assertions, if not their proofs, need to be encoded into the program in an effort to reduce the size of the output list. A difficulty here is saying the assertions in a comprehensible way which is well coupled to the original code. As you said previously, this probably requires an interactive system. -- John Skaller Felix, successor to C++: http://felix.sf.net