Re: [NOISE] was Re: java security concerns

["Perry E. Metzger" <perry@piermont.com>]

Peter Madden) (by way of Duncan Frissell <madden@mpi-sb.mpg.de> writes:
>  Applications of formal methods in software engineering depend
> critically on the use of automated theorem provers to provide improved
> support for the development of safety critical systems.  Potentially
> catastrophic consequences can derive from the failure of computerized
> systems upon which human lives rely such as medical diagnostic
> systems, air traffic control systems and defence systems (the recent
> failure of the computerized system controlling the London Ambulance
> Service provides an example of how serious software failure can be).

I far prefer trusting robust and failsafe engineering in such
situations. Theorem provers can't account for what happens when the
one in a billion DRAM corruption occurs, or someone kicks the cable
connecting the machine to its disks, or when a nut shoots the sensors,
or whatever. Well built systems fail in a safe manner because of good
engineering design -- as an example, in we hope that the motor
controller might die but the motor won't eat itself anyway no matter
what garbage it puts out. Such design is needed whether the systems
are "formally proven" or not -- and frankly, I can't see formal proofs
having much of an impact given that you are in the end simply shifting
the problem to bug-free specifications and yet still have to worry
about failures in the system.

Perry