Why I don't like formal methods...

I know the title of this port is a bit controversial and with it I alienate a lot of researchers, even at my own department. But I will try to clarify my arguments and hope that someone can prove them to be wrong.

• To be more precise; it is not the formal methods in itself I dislike, but the prominence they seem to have at prestigious software engineering conferences. I think it is not at all in proportion to how well-used formal methods are among professional development.
• Formal methods are really attractive from a researchers perspective. You can use concepts as theorem, proof and deduction and other nice things. But nice is not the same as relevant.
• Even though I have heard about formal methods as one of the enablers to establish software engineering as a "real" engineering discipline for almost ten years I still don't think they are nearer being well-established now than then.
• Some claim that you can never be sure of the software unless you can prove properties about it, and I agree that presently formal methods are the only technique that promises to do so. But there is a lot of successful software out there which have not been proven.
• Specifications that fulfil the requirement of being interpreted formally are hard to write. Compare it to learn a new programming language and be proficient enough to use it without any side effects.
• I don't know if formal methods scale well. It is one thing to use it on a nice prototype system with 30 entities developed in your lab. It is another thing to use it on a system with 500 entities, many of these with quite varying quality in requirements and code.
• I still don't know of any that uses formal methods for real; i.e. as part of the normal way in products shipped to customers in business intent on making money. Not in one-shot attempts, pilot projects or by non-profit organisations.
  A search on google skolar of industrial+software+formal+methods list papers from the 90s as the top results. And these seem more to be arguments against what I claim above rather than actual reports of usage. I really would welcome examples.