Formal methods can be used to specify, prove and generate code for an application. This is less prone to errors - thus mostly used in safety/critical programs.
Why don't we use it more often for everyday programming, or in web applications, etc... ?
References :
An Engineer is a person who can do with a dollar what any idiot can do with 10.
Resource constraints, budget constraints, time constraints, they are all important.
Developing software using formal methods is usually significantly more expensive and takes much longer than without. Also, for many projects, the hardest part is understanding the business requirements. All that using formal methods buys you in that case is proof that your code corresponds 100% to your incomplete and incorrect understanding of the business requirements.
For that reason, the use of formal methods, proofs, program verification and similar techniques is typically limited to "stuff that matters", i.e. avionics software, control systems for medical equipment, power plants, etc.
(-1 + 1) + INT_MAX = INT_MAX, -1 + (1 + INT_MAX) is undefined behavior.
Commented
Jul 28, 2018 at 22:08
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.
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:
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.
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.
Every program in any language can be thought of as a formal specification (equivalent to some turning machine). Any higher level 'formal specification' to be used in proving formal correctness is also - just another program. But its (typically) a bad, incomplete, vague, insufficiently thought through program. And not coincidentally, typically written by people who don't know how to program (they are usually domain experts).
And so proving that one program is compatible (produces the same answers or however you characterize it) with its higher level formal requirements, invariable comes down to how you resolve the ambiguities in the higher level formal specification. There is no good general purpose way to do that.
That mapping of high level requirements to lower level details is the gist of what real programming is about. It should not be surprising that the core work being done by a programmer reading and interpreting specifications cannot be replaced by hand-waving and saying 'now just see if this high level formal specification is complied to by this sample program'.
Even in the early days of logic programming, where this concept first seemed so promising (because both the high level specification and actual underlying programs could be written in the same language), this core problem proved intractable.
