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 programme using programming languages OR specify the programme 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: just google images for "What the customer wants" (for example picture here).
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 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 carful 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 side, it requires 2,3 times less efforts to get a high security software this way than with traditionally engineered software if you add the effort to make such software certified at high security level (EAL 7). So if you have high reliability or security requirements there is definitively a business case for going formal.