Delivery-Date: 
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: bulk
Date: Thu, 7 Apr 94 19:41:20 PDT
From: "peter v. homeier" <homeier@cs.ucla.edu>
Message-Id: <940408.024120z.19218.homeier@oahu.cs.ucla.edu>
To: info-hol@cs.uidaho.edu
Cc: homeier@cs.ucla.edu
Subject: How close is practical program proving?

I'd like to ask a number of questions, to get everyone's opinion on
the current state and future viability of software verification,
especially machine-assisted verification such as HOL can provide.

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?

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...)

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.

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?

It seems that with all the storm and fury about software verification,
there is a lot of sound but very little accomplished, in terms of verified
code.  There are some very good reasons for this, and I could contribute
a few, but I would like to hear what others think first.

And if you can contribute some good explanations of the difficulties, can
you suggest some ways we might progress to overcoming those difficulties?

So to summarize, can you tell me
  a) how close are we to some "programmers on the street" proving code?
  b) how close are we to expert programmers proving code?
  c) what makes program proving so hard anyways?
  d) can those difficulties be overcome, and how?

Peter Homeier
homeier@cs.ucla.edu