4

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
  • 4
    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
  • 1
    For projects that are extremely sensitive to potential errors, writing requirements/code at the amortized rate of one line of production code per person per month might well make sense. (The test code doesn't count, nor does the metacode doesn't count, nor do the formalized requirements. Production code only. With formal methods, it's easy to have the cost be the equivalent of a line of code per person per month.) For the vast majority of projects, "perfect is the enemy of good enough." – David Hammen Jul 17 '18 at 15:14
10

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
  • @jk. formal methods have been around for decades and their use in appropriate domains is actually well advanced. – Robbie Dee Jul 18 '18 at 8:20
  • @toto In fact, bugs, and human injuries and deaths, caused by bugs, are more expensive and time consuming than formal methods, most likely. For the space between "super critical code" and "stupid web app" some people are pushing for LIght formal methods, which are simply some subset of formal methods used on some subset of code, and generally favoring the friendlier tools. – Frank Hileman Jul 18 '18 at 17:39
4

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).

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 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.

  • 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
-1

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.