Software development: formal proof vs testing in the wild
What is the value of a formal proof for a program? Is a formal proof worth writing as you develop the software?
Defining what a software is
Software is a collection of changes to the code base, taken over a period of time. This is evident for anyone that uses a code revision system. By extrapolation, the future version of software is going to be a sum of this collection with another collection of changes each one created at various points in the time axis.
Software & Mathematics
Not all softwares are created equal. Some are created with a specific purpose to solving machine related problems. Whereas, some are created to solve man made problems such as Banking, Insurance, etc.. We have come a long way from solving problems of cracking Enigma. As the economy is moving more towards services & knowledge, more problems are being solved by Software. In this regard, this is a pertinent question to ask: is computer programming still confined to being a manifestation of a branch of mathematics?
Formal proof vs simple evidence
Mathematics demands formal proof and has it in place for almost every theory. The early software creators had a huge problem in their hand: efficiency. Due to hardware limitations, one has to write program closer to the hardware. Programming languages such as Lisp leaned towards mathematical way of doing things, whereas those such as Fortran/C leaned towards being more performant. Lisp and related languages are based on strong mathematics and the programs lend themselves such that writing proofs is a simple extension to writing actual code.
The programming world paid heed to the performance God. State machines were built without the worry of bringing the elegance of mathematics to the software world. We today talk about concepts such as Test Driven Development. A test is at best anecdotal evidences of code working as expected, and at worst they are hearsay (given the unpredictable nature of runtimes).
For a simpler analogy, the unit tests / integration tests are like your driver’s license tests. They are evidences that you can handle the car. But they are certainly not proof that you can drive the car absolutely well under all conditions. In comparison, can we employ similar techniques to certify an Auto Pilot system? Absolutely not! The evaluation parameters are very different and will certainly involve simulating all possible traffic conditions. Developing software for such a system is better served if formal proof is written for it.
The dilemma of unit tests vs formal proof
Functional programming, by virtue of being close to mathematics, provides easy ways to write proof. For an example of this, please check out this Haskell implementation of Parser Combinator. The system is a collection of functions that are absolutely deterministic. A parser combinator is a fundamental building block. The thing about fundamental building blocks are that they are narrow by definition and don’t change over time. In contrast, most production softwares change rapidly.
The hard question then is: when do you write formal proofs as opposed to just unit/integration tests. The question becomes significant because it has great implication on the productivity of an average computer programmer.
To understand any answer to this question better, we need to ask ourselves what exactly is a software first.
Software = Program + Context (world)
If you reach up to the earlier definition of the software, we stated that it is merely a collection of code diffs. However, this is incomplete. A software is created within a world as defined by the problem setters. This world has certain basic primitives which operate together to yield outputs in it. For the sake of clarity, let us take an e-commerce system. To name a few primitives in the world: user, product, order, payment, shipment. Most of what an e-commerce system does will revolve around these primitives.
But there is no guarantee that new concepts will not be introduced into this world. Say introducing a loyalty program to the mix so that every alternative purchase by the user will be delivered without a shipping fee. This is a change in the world. The rules of the game have been changed. To make this usecase happen, a programmer may need to introduce new primitives and define how the existing ones operate in a predictable manner with the new one.
Zoom out and you will notice that such a world will evolve quite significantly.
Some worlds don’t change (much!)
It is not always necessary that the world will change. OS Kernel and Drivers don’t change much. The C compiler doesn’t change much. InnoDB storage engine doesn’t change much. The word “much” is quite loaded in meaning and is to be considered with a lot of context.
Theoretically, even these softwares change but their purpose and the way they react to the events around them don’t change in any significant way. Most open source softwares solve problems that are very narrow by definition, examples being: message brokers, relational database, data compression, etc.. On the contrary, most commercial softwares (esp., those that target a man-made concept say Money & Banking & Shopping) are susceptible to a changing world.
Decreasing value of any given proof against the time axis
At any point in time, it is possible to prove that the software works as expected in the world it is defined in. However, as time progresses, software undergoes change either by itself (as improvements) or as a response to a change in the world. From a software creator’s point of view, Paid testing (QA team) of a snapshot of software is only useful to the extent that we minimise the testing with large unpaid users (customers). Zooming in, we see that the change of the software is merely a translation of a requirement created by the problem setter. It is unclear what changes will follow as time progresses. The current change may not be valid when the next change arrives. The proof is only valid for the current change. Read another way, the proof may not be valid for the changes that follow, thereby reducing the value of the current proof significantly.
More than 1 way to solve a problem
There are more than one ways to meet the requirements of the problem setter. It is easy to see this: if there be only one way to meet the requirement, then both the solution and the proof can be auto generated. However, this is not (yet) the case.
A generalised approach here: Abstractions are finite whereas concretions are infinite. Fractals are an excellent example here. Abstractions vs concretions maps elegantly to primitives (alphabets/grammar) vs contraptions (essays/prose/poems).
So, what does this mean?
The key observations we made in the previous segment are that changes are unpredictable, and there are more than 1 valid ways to implement a change. Taken together, it is impossible to prove that a current requirement tends to stay valid when seen against any future requirements.
The way forward
Procedural programming and most of functional programming that we see in the wild today don’t have formal proofs. The actual point is somewhere between calculated risk and leap of faith.
Today, functional programming has caught the imagination of many a developers. Functional programming has the potential to take us to a world where we can write programs more confidently. But I believe these are just early iterations. It is like a new toy that we are all fascinated with & want to play with. If we dig deep, we will be able to ask pertinent questions about software development. And hopefully, we will be able to employ the beauty of mathematics in a way that machines can be used more effectively at solving problems in the application domain rather than the systems domain.
For now, be adventurous and swing to the extremes, but do come back to rest in the middle! Keep writing great code!