Formal methods assume the difficult part of software development is producing code which precisely conforms to a specification. In reality the difficult part is to even get to an unambiguous specification with represent the actual business needs, which are often vague or unknown when development begins.
This lead to iterative development. But iterative development does not go well with formal methods. With vague specs and iterative development, the code itself ends up being the spec. If well-written, the code even reads like a spec, and during the iterative verification, it is proven if the spec/code conforms to the product owners actual (often unstated) requirements. Just take user interface design: It is incredible hard to design a good GUI for a complex application and requires multiple rounds of user testing and refinements. But if you actually have a spec for an UI, implementing it is trivial and can be done by the intern.
More fundamentally: If you do have the spec stated completely and unambiguous in a formal language...why don't you just compile the spec then? Seriously, why translate it by hand into a different language and then spend a lot of effort to prove you didn't make any mistakes in this translation? DSL's and declarative languages seem more promising as ways to bridge the gap between spec and code.
That said, there are obviously domains where formal methods are worth it, because you really want the extra verification in having the logic stated twice. Especially in hardware development which doesn't lend itself to iterative. It is just a small part of software development overall.
The most promising future for formal methods are in type system, since they are not separate from the code, so they lend them selves much better to refactoring.
This lead to iterative development. But iterative development does not go well with formal methods. With vague specs and iterative development, the code itself ends up being the spec. If well-written, the code even reads like a spec, and during the iterative verification, it is proven if the spec/code conforms to the product owners actual (often unstated) requirements. Just take user interface design: It is incredible hard to design a good GUI for a complex application and requires multiple rounds of user testing and refinements. But if you actually have a spec for an UI, implementing it is trivial and can be done by the intern.
More fundamentally: If you do have the spec stated completely and unambiguous in a formal language...why don't you just compile the spec then? Seriously, why translate it by hand into a different language and then spend a lot of effort to prove you didn't make any mistakes in this translation? DSL's and declarative languages seem more promising as ways to bridge the gap between spec and code.
That said, there are obviously domains where formal methods are worth it, because you really want the extra verification in having the logic stated twice. Especially in hardware development which doesn't lend itself to iterative. It is just a small part of software development overall.
The most promising future for formal methods are in type system, since they are not separate from the code, so they lend them selves much better to refactoring.