• It is true that I failed to mention "more advanced approaches, such as model checkers and satisfiability modulo theories solvers." There are hundreds of interesting techniques that I did not mention. They are valuable research results, but they do not constitute a software development method that is ready for widespread use. It is quite imaginative to assert that methods such as VDM and Z "blazed the trail" for model checkers and other decision procedures. The roots of that work are much older.
• It is true that there have been industrial applications of formal techniques such as the very recently published one that Dr. Pike mentions. As I wrote, the fact that these are research efforts, and the experience reports considered publishable, supports my claim that use of such methods is uncommon. Further, many methods check design models, not deployed code. Others are partial checks on existing code, rather than ways to develop provably correct code.
• It is true that many companies have funded research on formal methods; they began doing that at least 40 years ago. There has been limited success in some tractable areas such as protocol analysis, but application of the methods is far from "standard practice."
• It is true that some companies have used a nonstandard programming language on some projects and that some of these languages are clearly inspired by mathematics. The resemblance between these languages and the best known "formal methods" indicates that they have common roots—not that one inspired the other.
• It is true that many of the alternatives that I suggested were previously suggested by others. I raised those issues, not because I think they are new, but because I think they deserve more consideration than they get.