Delivery-Date: 
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: list
From: Konrad Slind <slind@informatik.tu-muenchen.de>
To: john.harrison@cl.cam.ac.uk, info-hol@leopard.cs.byu.edu
In-Reply-To: <"swan.cl.cam.:009180:950714233952"@cl.cam.ac.uk> (message from John Harrison on Sat, 15 Jul 1995 01:39:42 +0200)
Subject: Re: making theorem provers easier to use
Message-Id: <95Jul15.164031met_dst.8083@sunbroy14.informatik.tu-muenchen.de>
Date: Sat, 15 Jul 1995 16:40:30 +0200


> Consider the continued existence of LISP syntax, which is after all
> far removed from any mainstream mathematical or linguistic models.

It captures the language of finite trees and provides the basic
operations over them, plus McCarthy had the brilliant insight to
represent programs and data in the same syntax. Feferman has since
adopted it as the basis for some of his metamathematical systems, so I
would say that it can be viewed as the kernel of at least some
mathematical models.

Anyway, to address the wider discussion, by ENOD I think that most of
the impressive achievements in formal verification are due to the
persistence AND mathematical talent of the humans doing the
formalizations and proofs. The following fact is worth pondering: many
of the most significant verifications have been performed by people
working at an *extremely* low level of automation. It is not clear to me
that making proof systems with better user interfaces or more decision
procedures will change that. Sure the naive user can be supported for a
long time, but inevitably the user will be in a situation where the
support doesn't do the right thing or just plain isn't there. At that
point, the naive user is going to have a bad day.

Don't get me wrong: I believe that automatic support is good, however, I
don't think we should saddle ourselves with the pernicious belief that
better automatic tools will lead us to the promised land where
verification will be an easier task. We may be able to easily verify a
larger number of trivial circuits or programs, but remember that we are
trying to meet expectations that keep rising. We may make bigger steps
in proofs, but the decisions to be made will still require well-informed
and talented users.

The bad news is that verification will always be hard; the good news is
that it may be hard in more interesting ways.

Konrad.