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 06:20:08 +0100
Received: by dworshak.cs.uidaho.edu (1.37.109.4/16.2) id AA03398;
          Wed, 25 Aug 93 22:14:06 -0700
Sender: info-hol-request@cs.uidaho.edu
Errors-To: info-hol-request@cs.uidaho.edu
Precedence: bulk
Received: from Maui.CS.UCLA.EDU by dworshak.cs.uidaho.edu 
          with SMTP (1.37.109.4/16.2) id AA03394; Wed, 25 Aug 93 22:13:55 -0700
Received: from LocalHost.cs.ucla.edu 
          by maui.cs.ucla.edu (Sendmail 5.61d+YP/3.21) id AA11253;
          Wed, 25 Aug 93 22:13:52 -0700
Message-Id: <9308260513.AA11253@maui.cs.ucla.edu>
To: info-hol@dworshak.cs.uidaho.edu
Cc: John Harrison <John.Harrison@cl.cam.ac.uk>
Subject: Re: HOL improvement survey
Date: Wed, 25 Aug 93 22:13:50 PDT
From: chou@cs.ucla.edu


John Harrison wrote:

> As promised at the Vancouver meeting, I'm organizing a survey to
> collect views on how the HOL system should be improved.

Here's my two cents, which I'm posting publicly since I'm interested
to know whether anyone already has a good idea:

    How to make HOL proofs more readable and closer to the ordinary
    "textbook style" presentation?

I think many of you have experiences of the following kind.
You developed a theory a couple of months ago.  For some reason
you need to look at it again and modify it.  But you find that
you can't read your own proofs!  The only way you can revive your
memory is to step through the proofs using the subgoal package.
So all the efforts you spent on coming up with these proofs are lost.

One of the advantages of functional programming is that functional
programs, if well written, are rather readable.  I think we still
have a long way to go before the same readability is achieved in
machine-checkable proofs.

- Ching Tsun