Return-Path: <John.Harrison-request@cl.cam.ac.uk>
Delivery-Date: 
Received: from dworshak.cs.uidaho.edu (no rfc931) by swan.cl.cam.ac.uk 
          with SMTP (PP-6.5) outside ac.uk; Thu, 26 Aug 1993 16:33:21 +0100
Received: by dworshak.cs.uidaho.edu (1.37.109.4/16.2) id AA03637;
          Thu, 26 Aug 93 08:28:38 -0700
Sender: info-hol-request@cs.uidaho.edu
Errors-To: info-hol-request@cs.uidaho.edu
Precedence: bulk
Received: from swan.cl.cam.ac.uk by dworshak.cs.uidaho.edu 
          with SMTP (1.37.109.4/16.2) id AA03633; Thu, 26 Aug 93 08:28:33 -0700
Received: from dunlin.cl.cam.ac.uk (user lcp (rfc931)) by swan.cl.cam.ac.uk 
          with SMTP (PP-6.5) to cl; Thu, 26 Aug 1993 16:27:24 +0100
To: info-hol@dworshak.cs.uidaho.edu
Subject: Re: Computing in a Theorem Prover is Silly
Date: Thu, 26 Aug 93 16:27:06 +0100
From: Lawrence C Paulson <Larry.Paulson@cl.cam.ac.uk>
Message-Id: <"swan.cl.cam.:154730:930826152738"@cl.cam.ac.uk>


> Computing in a Theorem Prover is Silly

I couldn't agree more.  I prefer to use a pocket calculator.

But some proofs do involve elementary arithmetic.  It is nice to know that
defining a data structure for binary integers allows computations that would
be unthinkable using the Peano axioms.  The necessary definitions and proofs
are straightforward in practically any existing theorem prover, with no need
to wait for someone to invent a new architecture.

> flames to /dev/null, please

Again, I couldn't agree more.

							Larry Paulson