Delivery-Date: 
Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
Precedence: bulk
Date: Wed, 3 Mar 93 09:23:37 PST
From: Paul.Loewenstein@COM.Sun.Eng (Paul Loewenstein)
Message-Id: <9303031723.AA17554@lara.Eng.Sun.COM>
To: peters@edu.uark.mozart
Cc: info-hol@edu.uidaho.cs.ted
In-Reply-To: James Peters's message of Wed, 3 Mar 93 10:33:44 CST <9303031633.AA00648@mozart.uark.edu>
Subject: extracting code
Content-Length: 1382


James Peters writes:

> 
> To hol90/hol88 researchers:
> 
>    I am wondering if work is being done on the problem of extracting
> code from hol (hol90 or hol88) proofs.  I am hoping someone might be
> developing a version of hol (or a tool) similar to nuprl, which produces
> a lambda term during a nuprl proof.
> 
> Jim

I am not an "expert" in this field, but to extract code one needs
a *constructive* proof.  HOL is a classical logic and admits proof
by contradiction.

The extraction of an implementation from the proof of the existence
of something satisfying a specification requires an explicit witness
for that "something".  In HOL one can just derive a contradiction from
the assumption that nothing exists.  See my proof of koenig's lemma as
an example of an "essentially classical" proof.  The theorem is not
constructively derivable.

From what I have seen of constructive logics, and the difficulty of
introducing anything resembling theorem proving into engineering, I
think that constructive logics pose more problems than they solve
(at least from a hardware engineer's perspective).


Paul Loewenstein              Sun Microsystems Inc, Mailstop MPK 3-103,
Staff Engineer                2550 Garcia Avenue, Mountain View, CA 94043, USA
Formal Verification           Tel: 415-688-9664  FAX: 415-688-9565
                              paul.loewenstein@eng.sun.com