11

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 :

closed as primarily opinion-based by gnat, Jörg W Mittag, Christophe, amon, Robert Harvey Jul 17 '18 at 16:29

Many good questions generate some degree of opinion based on expert experience, but answers to this question will tend to be almost entirely based on opinions, rather than facts, references, or specific expertise. If this question can be reworded to fit the rules in the help center, please edit the question.

  • 3
    We could build houses with 5 foot thick walls - like medieval castles. Most of the time, that would be more trouble than it is worth. – Baldrickk Jul 17 '18 at 14:18
  • 5
    You can try applying formal methods to a web dev project, and see how it goes. Most likely you'll notice that you're pouring lots of effort into a low-value activity. Contrast that with quick smoke testing, which will already capture many bugs. Interestingly, static type systems are a simple kind of proof system, yet especially web development shuns those languages (instead preferring highly dynamic languages like Ruby, PHP, or JavaScript). Correlation does not imply causation, but it gives pause to thought. – amon Jul 17 '18 at 14:33
  • 1
    So you'd prefer to specify in a specification language instead of programming in a programming language ? Ok, you'll be able to prove that it works according to the specs. But how are you going to prove that the specification reflect the true problem ? – Christophe Jul 17 '18 at 14:36
  • 3
    @toto the question is: doing the things right (work according to the specs) or doing the right things (having the good specs). While in theory the spec is what we want, in practice we rarely know for sure what is really needed: beyssonmanagement.com/2012/10/29/… – Christophe Jul 17 '18 at 14:45
  • 2
    For those who are disappointed that this is closed there's now a great blog post: Why Don't People Use Formal Methods? – icc97 Jan 22 at 8:22
17

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.

  • I'd also add that putting formal methods into the programming language is an area of active research currently i.e. is not yet ready for mainstream – jk. Jul 17 '18 at 14:35
  • I accept this answer, but I also wanted an approach on why formal methods are still considered 'expensive' and 'time consuming', especially when we know how expensive is maintenance and code tracking/debugging on big projects. – toto Jul 17 '18 at 14:41
  • 1
    TDD & BDD are approaches built on the principles of Hoare logic, a foundation of formal approaches. They improve efficiency not detract from it. – Martin Spamer Jul 17 '18 at 15:00
  • 1
    @toto Proofs are really, REALLY hard. A lot of things mathematicians take for granted in proofs doesn't apply in programs. For example, in C++, addition is not associative: (-1 + 1) + INT_MAX = INT_MAX, -1 + (1 + INT_MAX) is undefined behavior. – Hovercouch Jul 28 '18 at 22:08
  • 1
    @toto: The reason they are considered "expensive" and "time-consuming" is because we can look at projects that are developed using formal methods and empirically verify that those projects take much longer to develop. Look at the development time of seL4/L4.verified, for example, compared to any other implementation of L4. – Jörg W Mittag Jul 29 '18 at 9:26
10

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:

enter image description 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 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).

In practice

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.

  • Contract based programming does use at least informal proofs. – Frank Hileman Jul 18 '18 at 17:41
  • @FrankHileman yes ! And the simple fact of clarifying preconditions, postconditions and invariants greatly helps to review code efficiently, reduce errors, and systematise tests. – Christophe Jul 18 '18 at 18:02
  • This should be the best answer by far. – Hashim Jan 22 at 2:59
0

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.

Not the answer you're looking for? Browse other questions tagged or ask your own question.