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 mail3-relais-sop.national.inria.fr (mail3-relais-sop.national.inria.fr [192.134.164.104]) by yquem.inria.fr (Postfix) with ESMTP id A52B8BC69 for ; Thu, 4 Oct 2007 23:00:49 +0200 (CEST) X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AgAAAHrwBEfAXQImh2dsb2JhbACOOAEBAQgKKQ X-IronPort-AV: E=Sophos;i="4.21,232,1188770400"; d="scan'208";a="3768169" Received: from discorde.inria.fr ([192.93.2.38]) by mail3-smtp-sop.national.inria.fr with ESMTP; 04 Oct 2007 23:00:49 +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 l94L0mbO015461 (version=TLSv1/SSLv3 cipher=RC4-SHA bits=128 verify=OK) for ; Thu, 4 Oct 2007 23:00:48 +0200 X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AgAAAHrwBEfLENaMnmdsb2JhbACOOAEBAQEHBAYp X-IronPort-AV: E=Sophos;i="4.21,232,1188770400"; d="scan'208";a="2393532" Received: from ipmail01.adl2.internode.on.net ([203.16.214.140]) by mail2-smtp-roc.national.inria.fr with ESMTP; 04 Oct 2007 23:00:46 +0200 X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AgAAAHrwBEd5LHvc/2dsb2JhbAAM X-IronPort-AV: E=Sophos;i="4.21,232,1188743400"; d="scan'208";a="204355749" 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 06:30:45 +0930 Subject: Re: [Caml-list] Unsoundness is essential From: skaller To: Ken Rose Cc: caml-list@inria.fr In-Reply-To: <470546BF.6020006@nc-sys.com> 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> <1191513834.6518.156.camel@rosella.wigram> <470546BF.6020006@nc-sys.com> Content-Type: text/plain Date: Fri, 05 Oct 2007 07:00:44 +1000 Message-Id: <1191531644.7078.121.camel@rosella.wigram> Mime-Version: 1.0 X-Mailer: Evolution 2.10.1 Content-Transfer-Encoding: 7bit X-Miltered: at discorde with ID 47055480.000 by Joe's j-chkmail (http://j-chkmail . ensmp . fr)! X-Spam: no; 0.00; compiler:01 compiler:01 prompts:98 sourceforge:01 assertions:01 assertions:01 wrote:01 wrote:01 caml-list:01 proofs:01 proofs:01 writes:01 partially:02 linear:02 output:02 On Thu, 2007-10-04 at 13:02 -0700, Ken Rose wrote: > skaller wrote: > > 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. > > > > > I think that in an industrial system, the assertions are going to have > to travel with the code. I can't imagine that a system that needs a > particular, highly trained programmer (the one who wrote the thing) to > cajole the compiler into generating code will ever be satisfactory to > any business that writes code. There is a such a system, I can't remember its name. The proofs and types etc do travel with the code, but the 'language' is designed with holes to fill in interactively, and the compiler fills them out partially then prompts for the balance. After supply, more holes are filled in by the same process. So for export, you get a complete linear representation of the conventional kind but you use a GUI to develop it. Perhaps someone can provide a link (it's quite well known very advanced category theory based system). -- John Skaller Felix, successor to C++: http://felix.sf.net