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: Easy theorem-provers -- not the Soft. Eng. answer
In-Reply-To: Your message of "Thu, 13 Jul 1995 15:00:46 PDT." <9507132200.AA13833@ice.cs.ucdavis.edu>
Mime-Version: 1.0
Content-Type: text/plain; charset="us-ascii"
Date: Thu, 13 Jul 1995 23:41:22 +0100
From: Donald Syme <Donald.Syme@cl.cam.ac.uk>
Message-Id: <"swan.cl.cam.:270680:950713224135"@cl.cam.ac.uk>


> My opinion on the making-HOL-easier-for-the-software-engineer is not to do
> so. I think that ultimately, verification (or least sophisticated,
> high-level code reasoning) will occur in an environment that has been 
> abstracted away from the underlying rigorous mechanized logic. The analogy
> is this: End-user application rogrammers (typically) don't write 486 or mips
> code, they write C++, or what not. Between the C++ programming environment 
> and the hardware are OS, library, and language implementation layers. This
> allows programmers to use tools such as debuggers that can talk about 
> "class Cell" or "integer variable ncells". I feel that we need to move towards
> a similar situation in code reasoning. Theorem-provers will have gargantuan,
> realistic specs of the language semantics, but the users will not interact
> with them directly. There will be layers and tools in between that provide
> a reasoning environment in which users can talk about familiar program objects,
> and moreover, they will be able to incorporate off-the-shelf algorithms
> (e.g. aliasing analysis, bounds checking, liveness...) into this environment.

Yes, spot on!  

For those interested, my ultimate research aim with TkHolWorkbench is
to experiment with providing (graphical) end user tools of the 
sort Rob suggests.  I think that most application
domains of HOL need really substantial work
done on visualisation and interaction tools
before these user-activity based end systems will 
arrive.  This means experimenting now and finding out what's involved. 

It's pretty easy to come up with lots of good ideas about 
what these end-user tools could look like.  But maybe it's time 
people in the theorem proving community really got stuck into 
implementing and experimenting with them?  Learning Tk or something
similar (Caml-Tk) might be a good place to start, if you've got a
spare week or three...

Don Syme