Delivery-Date: 
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: bulk
Date: Fri, 8 Apr 1994 13:35:03 +0930
From: Jim Grundy <jug@itd.dsto.gov.au>
Message-Id: <9404080405.AA19373@itd0.dsto.gov.au>
To: homeier@cs.ucla.edu
Subject: Re: How close is practical program proving?
In-Reply-To: Mail from 'info-hol-request@lal.cs.byu.edu' dated: Thu, 7 Apr 94 19:41:20 PDT
Cc: info-hol@leopard.cs.byu.edu

Peter Homeier asks several questions about the state of the art in producing
mechanically proved software.

I have a few thoughts:

> First of all, what programming languages have been formalized within
> HOL (or other theorem provers)?  Unity comes to mind, and Elsa Gunter's
> group has been working on SML.  Has anyone addressed more commonly
> used languages, such as C, Ada, or Pascal?

In HOL, Mike Gordon formalised a subset of a Pascal like langauge.
I have formalised a similar subset of a Pascal like langauge.
Joakim von Wright has formalised Dijkstra's guarded command language
(also a bit like a subset of Pascal, with some nondeterministic features).
The formalisation of such langauges is now not uncommon in HOL and other 
theorem provers.   Likewise, formalisation of functionally pure (no
side-effects) subsets of functional langauges is not uncommon.

Another approach to producing verified code is to have a system where
the formalisation of the langauge is outside of the theorem prover.
The tool is given the program and the specification, and by some magic produces
a Verification Condidtion which is then passed to a theorem prover for proving.
The langauges used with such systems tend to be a little more substantial.

Here are some langauge features that are difficult to formalise and are hence
relatively rare - you will find them - but generally not all together:
Pointers, Modules, IO, General Recursion

If you leave such things out, then there is little difference between the
remaining subsets of C, Ada and Pascal.

> For that matter, is there a translator from SML into C which preserves
> the semantics of the program?  If so, then one could presumably prove
> an SML program and then translate it into C.  (Of course, I can hear
> Elsa now saying, "But why would anyone *want* to translate from SML
> into C ??!!" ... and she may well be right.  It's a bit like ripping
> apart an evening gown to make dishrags...but if you need dishrags...)

I think there is, but the translator would not be proved, so what would you
know about the resulting C?

> The essence of what I wish to ask is this:  How close are we to the 
> day when a programmer can walk down to Egghead software, buy a "X"-language
> compiler and program verifier package, slap it into his home PC, and write
> and prove code for his personal projects?  I'm thinking of a programmer
> a bit above the average, with a taste and ability for logic, and with
> the patience required to attempt and complete a proof, and not simply 
> compile the stupid program.  I would not expect him to have a Ph.D. in
> Computer Science, or to be an expert in semantics of programming languages,
> or to take three years of his life to prove a 500-line program.

I don't think this is about to happen real soon now.  It may be doable soonish
for a very restricted language applied to a very restricted problem domain.

> OK, maybe that's asking too much.  Let me set an easier task.  How close
> are we to the day when a small start-up company with some really bright
> young guys and gals with Ph.D.'s or the equivalent can write and prove
> software applications or utilities that run on the first guy's home PC,
> and do something really useful, for which the verification contributes
> real value?

I suspect even this is quite a problem, its the really usefull stuff that is
the problem.   40 years ago things like calculating log tables and the like
were considered really usefull.   I dare say we could tackle that sort of thing
with ease.   In another 40 years perhaps we could do those things that are
considered really usefull today (I am being unrealistically pesimistic here -
I think we will do better than that) but nobody will be interested in doing
those sorts of things anymore.   Its very hard to reach a target that runs
away from you as fast as people's ambitions for computer applications does.

> c) what makes program proving so hard anyways?

1) Working with a simplified subset of programming languages is relatively
doable, (no pointers etc).   However, some features, are quite difficult
to provide a nice simple mathematical modle for - this makes proving things
about them hard.  Of course, it is often such features that destinguish the
real programs from the toy ones.

2) Computer programs are used to help solve problems from virtually every
problem domain there is.   This makes it very difficult to exploit domain
specific knowledge in program proofs.   Researches in general are reluctant
to concentrate their efforts on any one domain, that is say to give up proving
programs in general and concentrating on proving programs for process
control in particular - or if they do, their work is not regarded has
significant.

3) Just writing big programs on time and within budget (and that pass normal
acceptance testing) is hard, let alone proving them.

4) Theorem proving is the real killer.  It is easy enough to generate a
verification condition for a program (a proposition which if proved would
imply that the program met the specification), proving it is the hard thing.

5) Those applications that really demand the level of assurance delivered
though a program proof are the hardest to prove things about.   The real
justification for the effort of program proof comes from safety critical 
systems where bugs cause deaths.   However, such applications are typically
real time in nature and usually written in assembly code.   These things
are very hard to deal with.

6) Imperitive programs have state, this introduces a level of complexity not
usually fond in traditional mathematical proofs, or even proofs of hardware
or functional programs.

> d) can those difficulties be overcome, and how?

1) Don't try to write a progam and then prove it correct.   Design it to be
provable from the begining, and preferably you should view the programming
and the proving as the same task.   Decompose the design a bit - prove that
was a good step - decompose it some more - prove that - ... this is called
program refinement.   This techninque helps you break down the proof into
manageable hunks.

2) There needs to be more work done on the theorem proving end.   We need
provers that are as programmable as HOL, but which have tactics that are
more powerfull than the best current resolution provers like Eves.

3) We need user interface tools that help manage the size and complexity that
are associated with real programs.

4) We need to formalise slightly more complex programming lanaguges that have
modularisation features to help us cope with the complexity of large programs.


Well that looks longer than 2 cents worth - but that is probably all it is 
worth.

I reserve the right to be wrong or confused, but I hope the ideas above 
constitute a basis for discussion.

Jim

Jim Grundy (jug@itd.dsto.gov.au)