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 =================================================================