ion, reviews, rigorous procedures, regression testing, metrics, and so forth) have been helpful, but we are still dealing with an intrinsically unsatisfactory situation. Especially because there is, I believe, a serious alternative. Consider a mathematician who after working for many years produces a proof for a conjecture that has a length of several hundred thousand pages of semiformalized notations. Is the proof correct? Testing the proof by looking at a page here or there would allow us to find errors but would not yield a watertight conclusion. The situation would be similar if the mathematician wrote the proof in a formal language, say predicate calculus with set theory notations or any other formalism. Just looking at snippets here and there would still not settle the correctness (and one has to worry that the rigorous formalization actually corresponds with the conjecture to be proven, but let's ignore this for now). PAULWATSON Dennis de Champeaux Software Engineering Cons...