From: madden@mpi-sb.mpg.de (Peter Madden) (by way of Duncan Frissell <madden@mpi-sb.mpg.de>)
Date: Wed, 11 Oct 95 06:36:13 PDT
To: cypherpunks@toad.com
Subject: Re: [NOISE] was Re: java security concerns
Message-ID: <199510111335.JAA17959@panix.com>
MIME-Version: 1.0
Content-Type: text/plain



> Rather than trying to prove a program to be correct (which I agree is doomed
> to failure for the forseeable future for all but trivial programs)


I disagree: automatic program verification has come along in leaps and
bounds, largely due to the current research impetus in safety critical
systems. Various sorting programs, bin-packing programs, to mention
but a few, have all been successfully auto. verified (and these are
non-trivial programs, which form the building-blocks of even less
trivial "industrial-sized" programs).  Indeed, the technology has been
extrapolated to the automatic verification of electronic circuits,
compilers, schedule problems and computer configerations (all w.r.t. a
user's specification). The real problems lie with specifying the
program/problem correctly in the first place (so-called specifications
capture), and with automatic program *synthesis* from specifications
(which, in mathematical theorem proving terms, presents the problem of
creating existential objects, as opposed to just verifying that they
do the right job).

 I do, however, agree with the need/desire for a greater diversity of
program properties which can be automatically checked. 


Regards,

Peter

=================================================================

Dr Peter Madden,                                Email: madden@mpi-sb.mpg.de
Max-Planck-Institut fuer Informatik,            Phone: (49) (681) 302-5434
Im Stadtwald, W-66123 Saarbruecken, Germany.       Fax: (49) (681) 302-5401

=================================================================