One of my correspondents has said my comments on formal method (here and here) were too terse. There 
are a couple of things that annoy me about formal methods, but the lack of results is the foremost annoyance. After multiple decades of “research”, there should be at least one theorem that tells us something non-obvious about programs. The absence of such a theorem tells us something about the analytical capability of formal methods. About 10 years ago, I asked a formal methods list for an example of such a theorem and got nothing convincing. Remember “non-obvious” is a requirement so a complex re-statement of “a n element queue can be emptied in n steps” does not qualify.
Ambrose Bierce (photo above) defined cynic by: “A blackguard whose faulty vision sees things as they are, not as they ought to be.”