The Fifth Wheel of andrewg

I came across an article today that lifted my spirits:

100% Verifiable Bug-Free Code Is Possible (Dobbs Code)

The executive summary: ok-labs.com and nicta.com.au have developed a microkernel that is provably correct, in defiance of the conventional wisdom that formal methods are only practical for the simplest of projects. While I take my hat off to the developers for their heroic efforts, I firmly believe this is only the first step in a process that will revolutionise the industry. The ultimate goal should be a complete, provably correct computing platform. This will not come about quickly or easily, but there are practical things we can do in the meantime.

Recently, the SANS Institute published a list of the 25 most dangerous programming errors. Most of these, e.g. buffer overflows, are rookie mistakes that every apprentice programmer is warned about, yet even with better training and increased collective experience, the population of errors in the wild seems to increase daily. The reason is simple: as the number of programmers grows, and their productivity increases, the number of opportunities for errors to creep in grows faster than the ability of the human mind to be vigilant. Or to paraphrase Murphy’s Law: if a programmer can make mistakes, he will make mistakes.

The conventional wisdom is to accept that such errors will be made, and be vigilant in testing. But no amount of post-facto investigation can give us 100% confidence that a catastrophic error doesn’t lurk somewhere in the code. With software increasingly responsible for people’s lives (fly-by-wire aircraft, nuclear power), the potential consequences of code errors will become unmanageable. Let me demonstrate.

The standard equation of risk analysis is

risk = probability × severity

What this means in practice is that in order to maintain risk below a given maximum, any event that has N times more severe consequences (e.g. a plane crash that kills 10 times more people than a car crash) should happen N times less often. But going from 99.999% (five nines) certainty to 99.9999% (six nines) is a lot harder than going from 99% to 99.9%, due to diminishing returns. Throwing man-hours of testing at such a problem does not scale.

Formal methods give us a way around this impasse. But we do not even need the expense of formal testing to eliminate the most common errors – design choices in our programming languages can do a lot of the work for little cost. Consider the state of the art before the introduction of structured programming in Algol-60. Without nested loops or multi-line conditions, the GOTO statement was king. GOTO-based programming languages are Turing-complete, in that they can perform any conceivable algorithm, but they are too flexible. It is quite possible (and easy) to write nonsense algorithms where loops would start or end inside the ELSE block of an IF statement, for example*. No modern programmer would contemplate such absurdities – there was a very good reason why GOTO statements were banished from polite society. And yet programming languages without GOTO statements are still Turing-complete.

What the above history lesson shows us is that, given sufficiently intelligent design paradigms, we can remove once-thought-necessary features from our lexicon without sacrificing Turing completeness, and thereby eliminate entire classes of potential programming errors.**

Now consider buffer overflow – this can be generalised to all kinds of array bounds violation; a buffer being merely a 1D array. The array index is constrained between two values, typically 0 and some integer N. If the algorithm attempts to access the array with an index outside this range, we have an array bounds violation. If this is not tested for explicitly by the algorithm (easy for a stressed programmer to forget) or implicitly in the execution environment (inefficient and not always enabled) undesirable behaviour can easily result. We could laboriously check every subscription operation in our algorithm to ensure that sane values were being passed at all times; or we could change our programming paradigm so that it is impossible to write an invalid subscription operation.

This is not as outlandish as it sounds – we already have a commonly-used language feature that does most of the work for us: FOREACH. A FOREACH loop iterates over the elements of an array, and automatically stops when there are no more elements. We cannot pass an invalid value into the array subscription operation, because there is no such operation; subscription is handled implicitly by the FOREACH. If all buffer operations used FOREACH statements, there would never be an overflow.

Now say that at some point in the near future we find similar, implicit, methods for array subscription that cover all sensible use cases (in the same way we found alternatives for all sensible use cases of GOTO). We could then eliminate the explicit array subscription operation from our lexicon, and buffer overflows would be a historical curiosity.

I think such a development is within reach. Like many programming geeks I have been working, on and off, for some time on a pet language project which, amongst other things, features strict limitations on the array subscription operator, as well as a plethora of implicit alternatives to handle common use cases. I haven’t yet been able to eliminate subscription completely, but all ideas would be gratefully received.

* This is a real example from personal experience, which shockingly did work but was (unsuprisingly) impossible to understand.
** Of course, if the language is still Turing-complete, it will therefore still be possible to make the same error; but you will have to go out of your way to deliberately do so.