Re: [NOISE] was Re: java security concerns

> 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

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

Peter Madden) (by way of Duncan Frissell <madden@mpi-sb.mpg.de> writes:
> 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).

Bugs in specifications are just as easy for humans to produce as bugs
in implementations, and unfortunately there is no way for our machines
to psychically intuit what it was we wanted to specify that they do
any more than we can make them intuit what it was we wanted them to
do.

Remember, by the way, that in some sense a high level programming
language *is* a specification language. Authomatic synthesis from
"specifications" is just a higher level of programming language, with
all that entails.

Perry