Delivery-Date: 
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: bulk
Date: Mon, 11 Apr 1994 12:06:11 +0000
To: info-hol@leopard.cs.byu.edu
From: Andrew.Butterfield@cs.tcd.ie (Andrew Butterfield)
Subject: Re: How close is practical program proving? AND MORE
Message-ID: <"swan.cl.cam.:036450:940411112720"@cl.cam.ac.uk>

I forwarded some of this discussion locally to interested parties and got
this response:

from starovic@dsg.cs.tcd.ie (Gradimir Starovic):

--------------------

>
>
>Peter Homeier (HI, Peter!) asked how soon we could buy verification products
>for programming languages - and, more interestingly (to me), he asked what
>makes program proving so hard -
>


There are a few things that make program proving hard:

1. finding the right formalism for the real-world properties we want to 
   analyse (for the properties we think exist and are observable at the 
   low-level)

2. finding a way of managing the complexity - this is done with 
   abstraction/refinement *and* (de)composition - both have to be formally 
   defined, and what is important, to be appropriate for the properties 
   from (1)

Lots of other things, eg. it has to be easily available and user-friendly.

I don't know about HW, but there is so much SW today designed and developed
without any, or with using very little semi-formal verification, that such 
questions as above dont really mean much. We could give a list of approaches
which "solve" each of the above things, but considering the way the things are 
in the real world it may be better to make the goals much smaller. 


>
>so I think that part of the problem is the nature of the programming languages
>currently in use - they are still relics of old assumptions about the nature
>of computing - for example, explicit input and output statements are a
>historical artifact that result from old hardware designs that made knowing
>when your program or data was in core important - with modern paging, you
>almost never know - so they should all be changed to persistent or volatile or
>stream variables and assignments, and let the OS keep track of where they are
>... (more philosophy later)
>

This is again related to the level at which the specification is done. To 
verify a language runtime (which provides the abstraction of persistent 
objects for instance) you have to take into account that an object may be on
disk, or on a remote node, or the type of comms mechanism in use - things which 
may be transparent at the higher level (the "application code"). I dont think 
we can, in general,  say "such things are not worth verifying".


>Ching Tsun's question about which programs are worth proving implicitly
>assumes that program proving is very hard (otherwise, it would not be an
>interesting question) - but why should this be true?
>
>but nobody said anything about
>
>        how we write a specification in the first place
>        (i.e., what are we going to prove anyway?)
>
>        how paltry the mathematics is that supports this kind of analysis
>        (though Jim did mention the lack of simple mathematical models,
>        which is on the right track - i believe even more: that there isn't
>        even any sufficiently powerful mathematics to use for such models)
>

This is not entirely true, there are lots of known properties that are 
regarded as worth verifying, and work which describes categories of such 
properties, with an appropriate proof method for each category.
(I can give you some ref's if you are interested)


>Dr. Christopher Landauer
>

>Andrew Butterfield


Regards,
        Gradimir


Andrew Butterfield
_____________________________________________________________              
       
Dept. of Computer Science,                Location: WR.14.0.7
O'Reilly Institute,                      Tel: +353-1-702-1765
Trinity College,                         Fax: +353-1-677-2204
Dublin 2, IRELAND                Andrew.Butterfield@cs.tcd.ie
URL:          http://www.cs.tcd.ie/www/butrfeld/butrfeld.html