The trouble with formal specification is that for a lot of systems the specification is a substantial fraction of the length of the program it is meant to be sp

The trouble with formal specification is that for a lot of systems the specification is a substantial fraction of the length of the program it is meant to be specifying. In fact if you code in a high level language like Haskell it is actually possible for the code and specification to be the same length. At this point finding errors in the specification is just as difficult as finding errors in your code by inspection. What it comes down to is that a formal specification is a program we don't know how to compile. The exceptions to this are specifications that are non-constructive; they define an allowable behavior without defining how the result is computed. An example would be a specification for TCP that specifies that the data must be presented to the receiving program in the same order it was sent; the behavior is simple but the underlying mechanisms are complicated. However this is often not what the specification looks like. More usually its like the specification of a bank transaction, which says that afterwards the sending account must be debited and the receiving account credited. Well gee! The real problem is that the "correct" behavior of the program is complex and contingent, and making sure you have covered all of the issues during requirements gathering is very difficult. And you can't put a formal specification in front of the customer and say "Is this what you want it to do?" because they can't read it, any more than they can read source code.