Re: [NOISE] was Re: java security concerns

[madden@mpi-sb.mpg.de (Peter Madden) (by way of Duncan Frissell <madden@mpi-sb.mpg.de>)]

> 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

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