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:

• Mechanizing Proof – Computing, Risk and Trust, Donald Mackenzie.

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:

• They write the right stuff, Fast Company.