This is something of a philosophical note, imagining we have unlimited time to “ensure” that we produce perfectly correct software that fulfills all requirements.  In practice, we work under real world constraints, with evolving requirements and schedules and specifications, and we’re accustomed to producing results that deliver best value, where perfect is the enemy of the good (value).  We work on a curve of time vs quality, where the curve asymptotically approaches 100% quality with enough time, and we don’t want to be too far to the right on that curve.  We get diminishing returns for something we’ll never reach.  I’ll argue that even in theory with unlimited time, we will always be working on an asymptotic curve, and thus provably correct results and absolute certainty will always be out of reach.

Tests to the rescue (or not)

Let’s imagine a super simple function called “increment” that takes as input an unsigned 8 bit integer value, and returns the value plus one (rolling over to zero if the input value is 255).  There’s nothing special or interesting about this hypothetical function, other than that the range of possible inputs is small enough that we can trivially test all possible inputs to verify that the function produces the correct return value in every case.  We can do exhaustive testing, knowing that we will leave absolutely no corner cases untested.

Unfortunately, an obvious problem we face is that our testing could have bugs.  We could test our tests (which isn’t a bad idea), but then to approach greater certainty we could I suppose also test our tests for our tests, and then… test the tests for our tests for our tests…  We’re back to working with asymptotic certainty again.  Let’s ignore a potential need to test our tests (etc etc).   Significant bugs can exist in exhaustively tested code due to undefined behavior, at least in C and C++ and perhaps other languages.  When a program invokes undefined behavior, one possible result is that the program executes in exactly the way the author planned and hoped, and all tests of course pass.  This is not a good thing, since weeks or months or years later, upon changing the compiler, or the hardware used for testing, or the time of day, the executable could begin to fail.  But let’s ignore undefined behavior – for some languages it’s not an issue.  We still will need to consider that a bug in the compiler or a fault in the hardware might allow a test to pass when it should fail.  As a real world story, one machine learning program found the optimal solution on a (defective) development/test board was to use a short circuit that existed in the substrate of the board.  All tests passed, so long as it ran on the one-of-a-kind board.  As for compiler bugs and operating system bugs and bugs in any software we rely upon, we again get pulled into working with asymptotic certainty and trust, because those tools are built by developers that fundamentally face the same issues we do.

Maybe formal proofs of correctness to the rescue?  By now it’s obviously hopeless, but nevertheless, proofs have the same sorts of problems as software.  A proof itself could contain an error (aka bug). Even if we use automated verification tools for proofs, unfortunately, the tool used for verification could have a bug.  We’ll always be dealing with levels of trust.  Complete certainty is out of reach, and “good enough” remains.  In the end, we get back to trying to deliver the best value.  Most all the details of development are a means to that end.