Delivery-Date: 
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: list
To: info-hol@leopard.cs.byu.edu
Subject: Re: making theorem provers easier to use
In-Reply-To: Your message of "Fri, 14 Jul 1995 11:27:12 EDT." <9507141527.AA12739@ultrastar.EE.CORNELL.EDU>
Date: Sat, 15 Jul 1995 00:39:42 +0100
From: John Harrison <John.Harrison@cl.cam.ac.uk>
Message-Id: <"swan.cl.cam.:009180:950714233952"@cl.cam.ac.uk>


It's undeniably true that all of us spend too long directing HOL proofs at a
rather low level. Well, some of us do anyway. For example, my development of
real analysis consists of about 10000 lines of ML, and generates 170000
primitive inferences. 17 low-level inferences per line of ML doesn't suggest a
high level of abstraction from the underlying proof mechanisms. Is this a bad
thing? Well, up to a point low-level proofs can be educational. But the
attractions of solving trifling tautologies or arithmetic goals by primitive
inference tend to pall pretty quickly.

Why don't we write and exploit higher-level proof procedures more? OK there are
some, like inductive definition packages and arithmetic decision procedures.
But not too many. One possibility is that it's too hard to write them. It's
also often suggested that it will be too inefficient to decompose sophisticated
proof methods to lowlevel primitives. For an examination of these matters, see
my paper on reflection, advertised on info-hol fairly recently. I think a more
likely explanation is sociological; HOL hackers have simply got used to
low-level proofs. Why spend days writing a sophisticated decision procedure
when one can solve the cases at hand in an hour with a bit of spadework?

A related example: we *still* don't have a good automated tool for translating
between Classic ML, Standard ML and CAML, even though writing such a thing is
intellectually trifling. Someone could perfectly well take the initiative and
*do* it. It just so happens that nobody ever has. (I am uncomfortably aware of
the analogy with arguments that there was nothing wrong with communism, it was
just unlucky always to be badly implemented.)

Consider the continued existence of LISP syntax, which is after all far removed
from any mainstream mathematical or linguistic models. I'm not up to a detailed
exegesis of LISP's development, but I suspect that the prefix notation was
originally seen as a stopgap. Pretty soon though, people got used to it, and
even saw advantages in it. Generally speaking, bright, motivated people will
get used to almost anything if it has a beguiling intellectual simplicity. HOL
certainly has that (for some of us).

The lesson is, I think, that we need to spend less time in plug-and-chug proof
and more time reflecting on ways to make proofs easier. However we don't want
to move *too* far in the other direction: the plug-and-chug approach,
exemplified especially strongly by HOL and Mizar users, does at least mean we
acquire the experience which makes such reflection productive. Compare
Kreisel's ENOD slogan "Experience Not Only Doctrine".

John.