[Links Updated 6/2021]

The so-called experts will tell you it can’t be done; it is not possible to create bug-free software, at least at low-cost for a non-trivial application. Now it seems, we have our first documented case of ostensibly zero-defect software.

Last week, Government News Reported that Praxis High Integrity Systems, has created a 10,000 line zero-defect application for the National Security Agency; and has done so in a mere 260 person-days. That is nearly four times the oft-quoted average productivity rate said hold for software development. Better yet, the NSA is permitting Praxis to make the project materials available online to the public. Now a 10,000 LOC project is hardly monumental, but it is large enough to be a verification challenge; and is a far-cry from being trivial. I have done several embedded projects that were about this size.

A good deal has been written about the impracticality, if not impossibility of creating non-trivial zero-defect software. The obvious truth in this idea leads us to place our faith in a solid (and very expensive) validation and verification effort, which we hope will find all of the serious defects. Sometimes probabalistic methods are applied to attempt to predict the number of latent defects remaining in code, and the process is repeated until this number is low enough. Despite our dedicated attempts to overcome the inevitable imperfections in our software, probability on the scale of a single software artifact is imprecise; hope is a poor substitute for conviction; and now we have evidence that zero-defect (or at least near-zero-defect) code, may be, in fact, entirely feasible.

In 2003, a joint task force of industry and government organizations was formed to investigate and make recommendations on best practices for development of secure software. There are some pretty significant similarities between software security and software safety, and from my perspective, both areas are of interest. The result is a document entitled “Improving Security Across the Software Development Lifecycle”. This dense, 123-page document explored many aspects of the SDLC, as well as techniques used to mitigate errors throughout. It contains some very valuable information; but my primary focus today is on one very small aspect, and that is the development process. As it turns out, of all of the techniques and methodologies examined in this report, only two were able to show a significant demonstrable reduction in software defect count. First was the famed Team Software Process, as promoted by Watts Humprey and SEI. Second was a proprietary process known as Correctness by Construction from the folks who brought you SPARKAda; Praxis High Integrity Systems. The results of the two methods are difficult to compare, as different metrics are given for each; but it appears that TSP gives about a 90% reduction for the average project in which it is correctly used, whereas Correctness by Construction (hereafter abbreviated as CbC) has produced an average of 0.42 defects per KLOC averaged across 5 projects tracked from 1993 to 2003, with each project having progressively better statistics than the previous; and the last exhibiting zero defects over the whole 10,000 line application. Even the worst-case project, conducted in 1993, had 0.75 defects per KLOC; and this was for a substantially larger 197K line program. Compared to the average on a typical project of about 32 defects per KLOC (as given by “Best Kept Secrets of Peer Code Review (Modern Approach. Practical Advice.)“) this is a 43X improvement or a defect reduction of almost 98%; for their worst case example!

The report goes forward to state that CbC employs formal methods and issues the following caution: “Almost all US software production organizations know little or nothing about formal methods; some others are reluctant to use them. First, while for many methods the actual mathematics involved is not advanced, these methods require a mathematically rigorous way of thinking that most software developers are unfamiliar with. Second, as with TSP, they involve substantial up-front training. Lastly, the methods require the use of notations, tools, and programming languages that are not in widespread use in industry, thus requiring substantial changes from the way most organizations produce software today.”

Did you hear that guys and gals!? Software developers are not familiar with thinking in a mathematically rigorous way! What do you think about that? Well, believe it! Fortunately, the problem is simply lack of exposure. Most programming languages are forgiving, and permit us to think in logical short-cuts. It makes life a bit easier, and we usually get it right; but often, this can be where we get into trouble. Basically, formal methods tools require us to declare our intentions in detail, then perform consistency checks that makes sure we aren’t violating our own declared intentions.

I am of the opinion that any developer who can learn a new programming language paradigm (e.g. a C programmer who can learn Smalltalk; or a Java programmer who can learn Scheme), can learn to work within the framework of formal methods. It’s just a new perspective, with a more carefully constructed set set of rules.

So, here’s the thing. Zero-defect software is like the four-minute-mile… it was impossible until someone proved it wasn’t. The barrier has been broken. What’s more, it was broken with reasonably low cost, and the instruction manual has been laid out for you to follow. We should see a rapid progression of adoption, and progressively larger zero-defect applications being built; until its no longer news, but just the way things are done.

From this day forward, is there really any excuse for allowing software to ship with even a single bug? If someone is injured, or even just inconvenienced by a bug in some application of tomorrow, will the best army of attorneys be able to defend the producer against the lone expert witness who understands the implications of today’s development? Food for thought.

For a more critical review of the Tokeneer materials, see http://www.spinellis.gr/blog/ and don’t forget to read the comments, where Rod Chapman of Praxis addresses the criticisms, as well as some of the hype.

Oh, one more thing… Congratulations Praxis! Well done!

About Max H:
Max is a father, a husband, and a man of many interests. He is also a consulting software architect with over 3 decades experience in the design and implementation of complex software. View his Linked-In profile at http://www.linkedin.com/pro/swarchitect