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 discorde.inria.fr (discorde.inria.fr [192.93.2.38]) by yquem.inria.fr (Postfix) with ESMTP id 9925ABC0B for ; Wed, 31 Jan 2007 01:16:06 +0100 (CET) Received: from ipmail01.adl2.internode.on.net (ipmail01.adl2.internode.on.net [203.16.214.140]) by discorde.inria.fr (8.13.6/8.13.6) with ESMTP id l0V0G30K021595 for ; Wed, 31 Jan 2007 01:16:05 +0100 Received: from ppp27-234.lns1.syd6.internode.on.net (HELO rosella) ([59.167.27.234]) by ipmail01.adl2.internode.on.net with ESMTP; 31 Jan 2007 10:46:00 +1030 X-IronPort-AV: i="4.13,259,1167571800"; d="scan'208"; a="81528814:sNHT1120474138" Subject: Re: [Caml-list] Equality of functional values From: skaller To: Andrej.Bauer@andrej.com Cc: caml-list@yquem.inria.fr In-Reply-To: <45BFCF7D.5010302@fmf.uni-lj.si> References: <1170104645.4564.304.camel@penguin.local> <45BF471A.6060603@fmf.uni-lj.si> <1170165303.6391.20.camel@rosella.wigram> <45BFCF7D.5010302@fmf.uni-lj.si> Content-Type: text/plain Date: Wed, 31 Jan 2007 11:15:55 +1100 Message-Id: <1170202555.6391.161.camel@rosella.wigram> Mime-Version: 1.0 X-Mailer: Evolution 2.6.1 Content-Transfer-Encoding: 7bit X-Miltered: at discorde with ID 45BFDFC3.002 by Joe's j-chkmail (http://j-chkmail . ensmp . fr)! X-Spam: no; 0.00; 0100,:01 andrej:01 theorems:01 decidable:01 compiler:01 encodes:01 summarize:01 semantics:01 typeclass:01 axioms:01 quantified:01 run-time:01 theorems:01 tackled:01 coq:01 On Wed, 2007-01-31 at 00:06 +0100, Andrej Bauer wrote: > skaller wrote: > > Actually the idea 'equality of functions is not computable' > > is misleading .. IMHO. Equality of programmer written > > 'functions' should always be computable: more precisely one hopes > > every function could have a mechanically verifiable proof > > of correctness and wished programming languages provided an > > easy way to prove one. > > There are two major reasons why equality of functions might not be > computable in a specific situation: > > 1) Sufficiently general functions are allowed so that various > diagonalization theorems kick in and we get a proof that equality is not > decidable. You're right. Canonical example for me: my own Felix compiler :) [Encodes functions as data .. Felix language is Turing complete .. :] > 2) The functions are "simple", but they are represented in such a way > that they cannot be tested for equality. > > The first reason is more "theoretical" (but still underappreciated by > "real" programmers), :) I love this list because there are theoreticians who are ready to educate us 'real' programmers. > To summarize what I wrote above: it may be a matter of how functions are > represented, not _which_ functions we are trying to compare. You're right: that was a very nice explanation! > > BTW: Felix is one of the few general languages around that > > actually allows a statement of semantics: > > > > typeclass SemiGroup[t with Eq[t]] { > > virtual fun add: t * t -> t; > > axiom assoc(x:t, y:t, z:t): add(x, add(y,z)) == add(add(x,y),z); > > } > > > > These axioms are checkable: > > > > instance SemiGroup[int] { > > fun add:int * int -> int = "$1+$2"; > > } > > > > axiom_check(1,2,3); > > You are confusing checking of particular instances and checking the > general statement in which x, y and z, are universally quantified. The 'axiom_check' facility clearly only checks particular instances and would only provide a proof if you could exhaustively elaborate all such instances. > Checking of particular instances may still be valuable to a programmer, > though, as it is a form of run-time correctness checking. Yes. My experience is that it catches quite a lot of errors. Proof would be better .. but I don't know how to do that. > > however there's currently no way to state and prove > > theorems. It would be interesting if someone had some > > idea how to use one of the existing theorem provers > > to act as a proof assistant (verify user given proof, > > filling in enough 'gaps' in the formal steps to make > > it practical). > > I would go further: it would be interesting to augment real programming > languages with ways of writing specifications that can then be tackled > by theorem provers and proof asistants. I don't think you're going further .. I'm actually asking that question! I have looked at Coq, HOPL (light) etc, in the hope there is some way of using them to complete programmer proof sketches, but all still seem to need very heavy assistance beyond the understanding of a non-expert. > In the long run this might > educate programmers about the value of correct programs. Naturally, as > long as only Mars space probes and the occasional airplane crash because > of software errors, there won't be sufficient economic incentive to > wrote correct software. I believe that this isn't so: there is plenty of incentive to write correct software. Industry does monitor maintenance cost of software compared to cost of creating it. We don't need a plane crash to demonstrate the need for correctness, in fact that wouldn't help much because the costs aren't so easy to measure. Wages of people working on maintenance are measured regularly by all large organisations. Yet people still use PHP, Python, Java .. why? Industry may be stupid but it isn't *entirely* stupid :) -- John Skaller Felix, successor to C++: http://felix.sf.net