Why I don’t like formal methods…

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.

Leave a Reply

Your email address will not be published. Required fields are marked *