Return-Path: Delivery-Date: Received: from ted.cs.uidaho.edu (no rfc931) by swan.cl.cam.ac.uk with SMTP (PP-6.4) outside ac.uk; Wed, 3 Mar 1993 22:56:57 +0000 Received: by ted.cs.uidaho.edu (16.6/1.34) id AA14244; Wed, 3 Mar 93 14:35:09 -0800 Sender: info-hol-request@edu.uidaho.cs.ted Errors-To: info-hol-request@edu.uidaho.cs.ted Precedence: bulk Received: from cs.rpi.edu by ted.cs.uidaho.edu (16.6/1.34) id AA14239; Wed, 3 Mar 93 14:34:50 -0800 Received: from procyon.cs.rpi.edu by cs.rpi.edu (5.65c/1.2-RPI-CS-Dept) id AA25311; Wed, 3 Mar 1993 17:34:22 -0500 Date: Wed, 3 Mar 1993 17:34:20 -0500 From: musser@edu.rpi.cs Received: by procyon.cs.rpi.edu (5.65c/2.2-RPI-CS-client) id AA13705; Wed, 3 Mar 1993 17:34:20 -0500 Message-Id: <199303032234.AA13705@procyon.cs.rpi.edu> To: info-hol@edu.uidaho.cs.ted In-Reply-To: Paul Loewenstein's message of Wed, 3 Mar 93 09:23:37 PST <9303031723.AA17554@lara.Eng.Sun.COM> Subject: extracting code This is in response to both Paul Loewenstein's and Sreeranga Rajan's reponses to James Peter's question about work on extracting code from HOL proofs. The question of whether one is working in a constructive logic or not, in extracting code from proofs, is kind of a red herring. In a classical logic one can still (and usually does) write down proofs that are constructive, and from those proofs a program can be extracted. The important question is not whether the proof is constructive (it will be if it was written with the goal of extracting code from it) but whether is it a ``good'' constructive proof, in the sense of having a good (efficient) algorithm embodied in the construction it does. In this sense, a proof system can be viewed as a (rather high level) programming environment, in which one's first act after specifying the problem (stating it as an existence-conjecture) is to try to find a ``good'' constructive proof of the conjecture (assuming there is no bug (counterexample) in it), from which an efficient algorithm can be extracted (more or less automatically if the proof is detailed enough). In short, I don't think the fact that HOL is a classical logic is any hindrance to using it for programming-by-proving. The real issues appear not to be ones of theoretical limitation but rather of (1) understanding how to write good constructions and (2) engineering the proof system to be a usable programming environment. Dave =============================================================== David R. Musser Rensselaer Polytechnic Institute (518) 276-8660 Computer Science Department musser@cs.rpi.edu Troy, NY 12180 FAX: (518) 276-4033