This question already has an answer here:

I currently work in web development - unit testing, functional testing are all good and really are part of what is considered being a professional developer.

However, I also have a fear of flying and when on an aeroplane i often wonder what the development process is for developers on auto pilot or air traffic control systems is.

Obviously software is tested rigorously. But how?

Is unit testing conducted differently?, are there 2 x testers per developer etc etc.

Also - how the heck are functional tests completed in such an environment? Its definitely not a case of just hitting f5 on the keyboard :)

Most importantly, is there something that can be learned from the development/testing process for such applications that can be applied to more daily development tasks such as web development

marked as duplicate by amon, GlenH7, yannis Feb 16 '15 at 4:07

This question has been asked before and already has an answer. If those answers do not fully address your question, please ask a new question.


A substantial gap between business software and life-critical systems is the use of formal proof. Another is the strictness of the environment.

Formal proof

Tests are great to ensure that the system is free from known, identified bugs and that new features won't break existent ones (regression testing). However, the presence of tests doesn't imply the absence of bugs. Not if you have thousands of tests for a small program. Not if you have 100% line coverage and 100% branch coverage.

Formal proof, on the other hand, guarantees that the program works as expected. It's like proving a mathematical theorem: with such proof, you know that you get an expected result. Of course, proofs may contain errors which will report buggy code as correct or correct code as wrong; this is a different subject.

A basic example: a method takes two integers as parameters and returns an integer.

  • With ordinary testing, you will have unit tests which ensure the method returns the expected result for arbitrary “ordinary” values, say (2, 3) and for a few edge cases, say (0, 0), (-1, 3), (+∞, 3) and (+∞, -∞). And then, when QA department discovers that the method fails for values (7, -7), you may add a test for those specific values as well.

  • With formal proof, you will have a mathematical proof that the method returns the right value for (-∞..+∞, -∞..+∞). No unit tests can do that, because you will need an infinite number of tests for that testing for every possible value of both parameters.

What can you learn from this as a developer writing business software?

Frankly, not much. It's an interesting subject to study in theory, but is irrelevant in practice for business software. Originally, people thought formal proof would be the way we write software. Any software. Decades passed, and it appeared that formal proof has a cost so high, that it can be relevant only for life-critical software where a system failure leads not to millions of dollars lost by a company, but a death of one, ten, hundred of thousand persons and billions of dollars thrown away.

There might be one thing which may inspire programmers: code free of side effects. Without pushing as far as formal proof, the sole fact of understanding the basics of how the correctness can be proven may encourage the usage of functional programming. This often leads to code simpler to debug and often simpler to read.

For more information about the subject, read:

If you're interested by the subject, I highly recommend this book.

Strictness of the environment

  • When I write a small personal project, I don't care about requirements, or about correctness, or about code quality. I don't need it to be reviewed by pairs to check if everything is good. It's completely OK if it fails “in production”.

    If I find a bug, I don't care. I might resolve it, or may keep it.

  • Business systems require more attention. Requirements will be drafted, code will be carefully written, tests will reduce the risk of regressions, linters will check code on every commit to reduce risks of stupid errors, other team members will review my code, usually in an informal way.

    If a bug is found, it's not a big deal. A ticket will be opened, a programmer will be assigned and will either solve the bug or postpone it if he considers it to be too unimportant.

  • Life-critical systems receive much more care. There will be not one, but multiple reviewers. Formal reviews will be done. Linters are not enough, and powerful static checkers will try to find the slightest error. Testers will explore any opportunity to crash the system.

    If a bug is found, the whole workflow is restudied. What we did wrong? Why the bug appeared in the first place? Why static checkers were unable to discover it? Why testers missed it? More importantly, what can we do now to prevent similar bugs from appearing in the future? Will another static checker help? What if a different form of formal review could have helped to discover the bug?

What can you learn from this as a developer writing business software?

I would consider two things, but both are more important for project managers and team leads rather than programmers themselves:

  1. It's never someone's fault. I've seen managers running in the room and screaming at a programmer who inadvertently introduced a bug which had major consequences in production. Well, great manager you are, that's the way to treat people. Especially since the project has no tests, there are no code reviews and no static checking, because all this is considered a waste of time by the company.

    If there is a bug, it means that the author of the code, the testers, the code reviewers and the static checkers all failed. Or the company failed to learn how to develop software correctly by considering testing, code reviews and static checking as not important.

  2. When the product is bad, probably the process itself is bad. Improving the workflow can make a huge difference, and in a presence of a bug, one should ask himself how could it happen that the bug was not found before the software reached production.

    Chances are, the change within the workflow could have been helpful in avoiding this bug, as well as dozens or hundreds of other bugs that are here, right now, in the code base, waiting to be discovered.

For more information about the subject, read:

  • "Frankly, not much." I wouldn't go so far as to say that. The cost of applying formal proofs to an entire program is exorbitant, but applying proofs to individual functions isn't all that hard and I'd argue any developer that's not at least somewhat familiar with it is doing himself at disservice (in the same way that everyone should have at least some knowledge of Big O notation.) If you wrote the code you're already halfway to a proof anyways, since you wouldn't have written it if you didn't think it did the right thing. – Doval Feb 16 '15 at 0:47
  • "applying proofs to individual functions isn't all that hard": according to the book I linked to in my answer, it's very hard. Not mentioning that you need specific hardware and OS which was verified as well. I imagine you are talking not about formal proof per se, but something else, such as a manual check that the implementation of the algorithm looks correct. – Arseni Mourzenko Feb 16 '15 at 0:59
  • I'm talking about using, say, structural induction to prove code that manipulates trees is correct or Hoare logic to show that a loop calculates the correct result. It's not exactly rocket science. It gets crazy expensive when you require every line of code to have a proof and every proof to be checked. – Doval Feb 16 '15 at 1:07
  • @Doval: I understand. Indeed, such partial verification is possible. One should note still the partial aspect: if your code is proven to be correct, (1) the language, compiler and framework are not verified, neither do (2) the hardware and OS. – Arseni Mourzenko Feb 16 '15 at 1:17

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