Did you also send this post to cypherpunks@toad.com?
No I didn't -- wasn't sure if that's where F. Stuart's email originated from. Please feel free to circulate to the universe, along with some further clarification below. I hope I wasn't too positive in my support of auto. program verification. There are real problems. However, with the development of the field called formal methods, computation has been directly linked to mathematical logic, which is a much better understood, and well circumscribed, domain than programming languages per se. 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). Formal methods are used to provide programs with, or prove that programs have, certain properties: a program may be proved to terminate; two programs may be proved equivalent; an inefficient program may be transformed into an equivalent efficient program; a program may be verified to satisfy some specification (i.e. a program is proved to compute the specified function/relation); and a program may be synthesized that satisfies some specification. Program Verification boils down to proving a mathematical conjecture specifying that a given program will, for all inputs of a certain type, generate outputs of a certain type. This is relatively straightforward -- we already have the program P described in the initial conjecture to be proved. Program synthesis, on the other hand, starts with a similar conjecture *except* that P remains an unidentified variable. The task of synthesis (auto. or otherwise) is to incrementally identify P as the conjecture proof is unraveled. This requires all kinds of "intelligent", and often intuitive, choices during the proof, and is consequently a difficult process to automate. 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 =================================================================