To program or not to program?
To solve a problem with a software product, after having an understanding of the requirements, you can EITHER write a program using programming languages OR specify the program using a formal language and use code generation tools. The latter just adds a level of abstraction.
Doing the things right or doing the right things?
The formal approach gives you a proof that your software works according to the specifications. So your product does the things right. But does it do the right things?
The requirements on which you are working might be incomplete or ambiguous. They could even be buggy. In the worst case, the real needs are not even expressed. But a picture is worth a thousand words, just google images for "What the customer wants", for example from this article:
The cost of formality
In a perfect world, you would have fully detailed and perfect requirements from the beginning. You could then fully specify your software. If you'd go for formal, your code would be generated automatically so that you would be more productive. Productivity gains would offset the cost of the formal tools. And everybody would now using formal methods. So why isn't it?
In practice, this is rarely the reality! This is why so many waterfall projects failed, and why iterative development methods (agile, RAD, etc) took the lead: they can handle incomplete and imperfect requirements, designs and implementations and refine them until they are fine.
And here comes the point. With formal methods, each iteration requires to have a completely consistent formal spec. This requires careful thinking and additional work, because formal logic is not forgiving and doesn't like incomplete thoughts. Simple throw-away experiments become expensive under this constraint. And so does each iteration that would lead to backtracking (e.g. an idea that didn't work, or a requirement that was misunderstood).
When not obliged to use formal methods for legal or contractual reasons, you can also achieve very high quality without formal systems, for example by using contract based programming and other good practices (e.g. code review, TDD, etc...). You'll not be able to prove that your software works, but your users will enjoy working software sooner.
Update: measured effort
In the October 2018 issue of Communications of the ACM there is an interesting article about Formally verified software in the real world with some estimates of the effort.
Interestingly (based on OS development for military equipment), it seems that producing formally proved software requires 3.3 times more effort than with traditional engineering techniques. So it's really costly.
On the other hand, it requires 2.3 times less effort to get high security software this way than with traditionally engineered software if you add the effort to make such software certified at a high security level (EAL 7). So if you have high reliability or security requirements there is definitively a business case for going formal.
seL4 design and code development took two person-years. Adding up all serospecific proofs over the years comes to a total of 18 person-years for 8,700 lines of C code. In comparison, L4Ka::Pistachio, another microkernel in the L4 family, comparable in size to seL4, took six person-years to develop and provides no significant level of assurance. This means there is only a factor 3.3 between verified software and traditionally engineered software. According to the estimation method by Colbert and Boehm,8 a traditional Common Criteria EAL7 certification for 8,700 lines of C code would take more than 45.9 person-years. That means formal binary-level implementation verification is already more than a factor of 2.3 less costly than the highest certification level of Common Criteria yet provides significantly stronger assurance.