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