This is dated 1999. It seems that agile methods have become more popular over that time, and upfront approaches (like formal methods) less so. One could interpr

This is dated 1999. It seems that agile methods have become more popular over that time, and upfront approaches (like formal methods) less so. One could interpret that unpopularity as the failure of formal methods... or as suggesting an untapped vein of problems that are too complex to solve without formal methods. Popularity != Merit (see Knuth: http://news.ycombinator.com/item?id=3390760 http://news.ycombinator.com/item?id=3390760) [myth 2] No program was proved [...] [The] process of formal development of the TD helped a lot in finding omissions, ambiguities, inconsistencies and incompletenesses in the informal descriptions. [myth 4] [Mathematicians'] solutions were so short and tricky that nobody else [...] could read them. [...] If specifications are not written using the same style it is almost impossible for implementers and testers to read them efficiently and effectively. BTW: It's striking how lisp combines aspects of agile and formal methods, in terms of hacking and a mathematical-like approach, combining both good and bad aspects.