Delivery-Date: 
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: list
Message-Id: <9507132200.AA13833@ice.cs.ucdavis.edu>
To: info-hol@leopard.cs.byu.edu
Subject: Easy theorem-provers -- not the Soft. Eng. answer
Date: Thu, 13 Jul 95 15:00:46 -0700
From: shaw@cs.ucdavis.edu


Hi all.

[begin Grandiose mode]

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.

Clearly I'm talking many years down the road, but I think this is the 
direction in which we must begin moving today. Just are there are architects,
OS people, compiler people; there will be theorem-prover people, semantics
people, and so on... 

Rob Shaw