This is an old post which I rehash since I still think the topic is relevant. I know the topic of is a bit controversial and with it I alienate a lot of researchers and some practitioners. 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. This scientific paper seems to have analysed currrent trends, but I would welcome examples that did not require a subscription to Springer.