Myths about Formal Methods in Software Engineering?

There are two widely cited papers that discuss philosophical issues of formal methods in software engineering in an interesting context:

Related comments appear in J. A. Goguen & Luqi, "Formal methods and social context in software development", TAPSOFT '95: Theory and Practice of Software Development, Springer-Verlag, Lect. Notes in Comput. Sci., V. 915, 1995, 62-81.

We might choose to ignore formal methods if they were irrelevant to the construction of quality software -- experience argues to the contrary. But uncertainty in the meaning and role of "formal methods" is wide-spread. The discussions in the literature cited here is intended to identify and elucidate some common observations in this regard.

The dictionary meaning that appears to most closely reflect the intention of the word 'myth' in the titles (and content) of the papers cited above is "a fiction or half-truth". Presumably this meaning is hence also accurately rendered as "a falsehood or a half-lie". Regarded from this perspective, the myths (if correctly so categorized) can be viewed as a "laundry list" of aspirations and limitations of formal methods. We briefly list the entire collection of myths here and feel that the essence of much commentary about formal methods is effectively communicated by a succinct phrase. The reader is encouraged to consult the original sources for extended discussion pro and con.

Myth 1 (Hall): formal methods guarantee perfect software and eliminate the need for testing.

Myth 2 (Hall): formal methods are all about proving programs correct.

Myth 3 (Hall): formal methods are only useful in safety-critical systems.

Myth 4 (Hall): application of formal methods requires highly trained mathematicians.

Myth 5 (Hall): applications of formal methods increases development costs.

Myth 6 (Hall): formal methods are unacceptable to users.

Myth 7 (Hall): formal methods are not used on real large-scale systems.

Myth 8 (Bowen & Hinchey): formal methods delay the development process.

Myth 9 (Bowen & Hinchey): formal methods are not supported by tools.

Myth 10 (Bowen & Hinchey): formal methods mean forsaking traditional engineering design methods.

Myth 11 (Bowen & Hinchey): formal methods only apply to software.

Myth 12 (Bowen & Hinchey): formal methods are not required.

Myth 13 (Bowen & Hinchey): formal methods are not supported.

Myth 14 (Bowen & Hinchey): formal methods people always use formal methods.