Channels ▼


Longing For Code Correctness

When I was young and first got into programming seriously, I reveled in working at the lowest levels of code. I loved (loved!) assembly language and could think of no greater happiness than doing clever things with registers and writing tight, fast code that squeezed into the minimum amount of RAM and delivered great performance.

More Insights

White Papers

More >>


More >>


More >>

As time passed, the lack of portability and the burden of learning the ins and outs of every new architecture got me interested C. In C, I thought I'd finally found the gateway to paradise: portable assembly language. What could possibly be better?

But after nearly 10 years of working in C on my personal projects, I tired of never being able to bring anything to a close, unless the project was a minor utility. Anything bigger never bore the full elements of my original ambitions. Feature lopping was a common practice. And even then more modestly resized projects, under unsparing hours in the debugger, would eventually be consigned to the groaning shelf of unfinished projects.

I had to move on. I went to Java, which drew me with its siren song of portability, performance, excellent tools, and enormous libraries. Not having to code one more linked list had remarkable appeal. So did the superior testing tools that would allow me to write code and test it quickly. This enabled me to avoid spending lots of time in the debugger. Ever since, Java has been my base language for personal projects, both large and small. (I am not implying that it will be my final destination. I continue to be troubled by the inconvenience of delivering software to non-developer users, who are not at all comfortable downloading or updating Java. A garbage-collected, portable, binary language with good libraries that is not as complex as C++ has great appeal to me. Which is certainly why I feel so interested in Go at the moment.)

As time has passed, though, I've found myself constantly frustrated by the feeling that no matter how much I test my code, I can't be sure with certainty that it's right. The best I can say is that the code is probably right. But when I write code for others to use, I want it to be completely reliable. This concern has led me to embrace tools that enforce the correctness of the code.

Long ago, for example, I adopted Bertrand Meyer's concept of design-by-contract (DBC), which suggests that every function should test for pre-conditions, post-conditions, and invariants. In Java, I do this with the excellent Guava library. So my methods tend to have tests, especially at the beginning where each parameter is carefully checked. I test invariants and post-conditions primarily in unit tests, which is probably not ideal, but it moves some of the validation clutter out of the code.

I'd like to go beyond this. First, I wish the languages provided better support for correctness. For example, I think floats should default to an uninitialized value of NaN (not a number). I wish integers had a NaN equivalent and that all primitive data types and strings had an invalid value to which they would be initialized by the language. A whole class of errors would go away. (In the absence of this, the Java compiler's ability to identify uninitialized values is undeniably helpful.)

But moving beyond these simple levels is where things become a lot more difficult. I have essentially two major options. The first would be to code in some kind of modeling language. Then use a tool, such as Conformiq's products or others, to generate thousands of tests. Then, automatically generate the code from the models and run all the tests. This is a highly effective way of writing solid code, and it is favored widely in Europe. However, I'm a coder at heart, and I'm not sure coding at a diagrammatic level is really my cup of tea.

The second alternative is to use languages that strongly support correctness. There are not many. Ada goes farther than Java in this regard. And Eiffel perhaps farther yet. But probably the one that does the most is Spark, an Ada subset. Developed in the U.K., Spark uses a system of annotations that are embedded in comments at the start of each method. The code can then be verified by assorted tools that check it against the annotations. Free and commercial versions of SPARK tools exist today.

Specifying code functionality in this way is undoubtedly an extra step with lots of additional typing involved. But it has advantages outside of proving correctness: To start with, it more fully documents the code. And, as Edmond Schonberg (formerly a professor of computer science at NYU and now an executive at AdaCore) mentioned to me in a pick-up conversation, by writing out the specifications before the code, most of the same benefits that tests deliver to TDD aficionados accrue to coders — the tests or specifications force you to spell out what you're doing before you begin to code. "Lots of defects get caught by this simple step," according to Schonberg. I believe it.

And I rue that in the U.S., only a few industries (mostly embedded, automotive, and avionics) are interested in high levels of code correctness. It's a topic that is dismissed as a luxury by mainstream programmers because it appears to interfere with the ability to deliver software quickly.

I have some sympathy for this point of view. If I were to indulge my desire for correctness more deeply, I would certainly want to have a scripting language as a secondary tool for testing out ideas and banging out code that doesn't need to be perfect. I don't want correctness to push me back to the days of coding in C when nothing was ever completed. However, as the recent Knight Capital disaster on Wall Street demonstrates, the general resistance to correctness felt by business programmers is a conceit that cannot always be accommodated without considering its occasionally dire consequences.

— Andrew Binstock
Editor in Chief
Twitter: platypusguy

Related Reading

Currently we allow the following HTML tags in comments:

Single tags

These tags can be used alone and don't need an ending tag.

<br> Defines a single line break

<hr> Defines a horizontal line

Matching tags

These require an ending tag - e.g. <i>italic text</i>

<a> Defines an anchor

<b> Defines bold text

<big> Defines big text

<blockquote> Defines a long quotation

<caption> Defines a table caption

<cite> Defines a citation

<code> Defines computer code text

<em> Defines emphasized text

<fieldset> Defines a border around elements in a form

<h1> This is heading 1

<h2> This is heading 2

<h3> This is heading 3

<h4> This is heading 4

<h5> This is heading 5

<h6> This is heading 6

<i> Defines italic text

<p> Defines a paragraph

<pre> Defines preformatted text

<q> Defines a short quotation

<samp> Defines sample computer code text

<small> Defines small text

<span> Defines a section in a document

<s> Defines strikethrough text

<strike> Defines strikethrough text

<strong> Defines strong text

<sub> Defines subscripted text

<sup> Defines superscripted text

<u> Defines underlined text

Dr. Dobb's encourages readers to engage in spirited, healthy debate, including taking us to task. However, Dr. Dobb's moderates all comments posted to our site, and reserves the right to modify or remove any content that it determines to be derogatory, offensive, inflammatory, vulgar, irrelevant/off-topic, racist or obvious marketing or spam. Dr. Dobb's further reserves the right to disable the profile of any commenter participating in said activities.

Disqus Tips To upload an avatar photo, first complete your Disqus profile. | View the list of supported HTML tags you can use to style comments. | Please read our commenting policy.



Building bug free software is not viable. Customers, within limits, would rather have cheap buggy software today than bug free code years from now. The issue is compromise. Many software applications have a lifetime. The aim is to try to build software so that the bugs are not show stoppers. Also while proper training can help, not many programmers are well trained and the ones that are either too expensive or moved up the ladder.


Problem here: Incorrectness costs a lot. Trying to remove incorrectness after the fact costs even more. The cheapest way is to build correctness into the code.


Did you ever read "Writing Solid Code" of Steve Maguire?
Right code is also a question of good coding style and does not only depend on the programming language ... ;o)


Software Engineering has been in crisis since 1970, how could you say have done well, maybe I miss something, but can you explain that cost of software has gone up exponentially and computers has been growing down ever since. It's simple the hardware has been maintaining the cost of computing while software is a merely survivor industry, just giants can survive. You don't need to hide bugs the languages are so bad that you can't find them without putting you paying a high cost of testing


The academic exercises of mathematical proof of "program correctness" may not be practiced, but they DO educate the principles and usage of pre-conditions, post-conditions, and invariants. This is a great example of where academic "exercises" are not directly applied in the "real world", but some of its core concepts can (should) be applied in day-to-day professional coding practice.


I think you are very correct in your observations. Businesses want their software as quickly as possible and understandably so. Time is very much money and money and time without tools is a drag on the core function of business -- making money from delivering products and services. So, there is a deep motivation by business to deliver.

This profit motive needs to be tempered and that requires a correctness evangelist who can instill the appreciation of the illusion of Rapid Application Development -- it is usually not true.

Programmers and coders fall for the trap of RAD as well. They are lulled into the false sense of security in their own skills and perceptions of what they can deliver, when and of what quality it will be when they do. My personal experience is that I tend to underestimate by about 4 to 5 times the actually time and money required to deliver quality.

When this notion first hit me, I opted to say, "Take my first ball-park estimate and double or triple it." Today, I typically like to say, "Take my first ball-park and multiply by a factor of 4 to 6 and perhaps more!" While this is sticker shock to the business owners, the notion has served me well.

Our present project was estimated at 18-24 months on this paradigm. Several months back, we were introduced to even more specifications that went hidden due to a lack of communication that took 3 months to figure out and estimate and will add another 6 months or so to the project. This means the original estimate jumped to 33 months (24 + 3 + 6).

Nevertheless, we are building code that is highly correct and very solid. From that platform, we are discovering that once you have correctness flowing well, the brains of the team can turn to the real core issues of the project: GOOD DESIGN! Personally, I find it more challenging to get to good designs than I do to code that is technically correct. So, if correctness includes both technically correct and business correct and design correct -- getting good designs is the greater challenge.


We have been using Dr. Bertrand Meyer's Eiffel and Eiffel Studio since November 2010. I can speak to software correctness and specifically Design-by-Control from day-to-day experience. After 20 years of other languages without DbC and the new Auto-test suite, I would be hard pressed to code in any language technology without these tools. Based on this, I would like to speak to a few points Andrew has presented above.

First, having a correctness-friendly project team is a matter of choice, requiring project leaders to be part technologist and part techno-evangelist. Business leaders need someone willing to tell the hard and difficult story of software disasters and to preach the virtues of software correctness. This must happen with technologists who live close to the people holding the projects purse strings. Mostly, it is an instilling in them of, "This is the right choice. You will NOT regret making this choice!" -- and then working like heck to ensure they do not.

Second, appreciation of correctness must be experienced. However, getting to meaningful experience requires being led and mentored by someone having walked the road. Why? Because a clearer understanding of correctness in the day-to-day workplace is counter-intuitive. Personally, I press myself to write contracts like a contract fanatic.

Third, I have learned how contracts (at least in Eiffel) are most effective when they are about more than just routine argument checking. Each contract consists of both a descriptive tag and an assertion. Both the individual contracts and the pre-condition, post-condition and invariant blocks (taken together) can we written in such a way that they convey the business intent of a class from the core parts of a system to its externally facing API's.

Fourth, contracts are only one part of the ordinance available in the correctness arsenal. Multiple inheritance, generic classes and Void safety are powerful tools in the hands of a designer -- not just a coder.

Fifth, the compiler is the glue that holds all this together! I am unaware of a compiler as strong as the one in Eiffel Studio version of Eiffel. For instance, not only does the compiler pick up on static coding errors, but gives spot on advice on how to correct those errors. Consequently, I have found that I can write very significant code and even refactors and have the code run the first time without error (syntactical or logical) more often than not.

Finally, as much as I am now firmly settled on Eiffel as my development technology of choice, I can say firmly that my deepest commitment is to a culture of quality and correctness because it is good for business and best serving the needs of my customers and their customers.


I am surprised that you have not mentioned Dijkstra's 'Discipline of Programming'; a tough read, but highly satisfying. CAR Hoare et al. spoke about the 'Axioms of Programming.'
But correctness like quality takes time and money. Large companies have rough estimates of how many uncovered bugs there are in their product after they have stopped support. The aim is not to produce correct software but to reduce the probability that a bug will manifest itself. So far we (software engineers) have done well. Very few accidents are caused by software bugs. Compared to the cost of correct software, testing and bug fixing appear cheaper.
This cannot go on indefinitely, although we have a long way to go before correctness becomes critical.


Problem with C was always it was a backwards step from ALGOL. C was not a safe language - you could write C code to undermine the systems you had written in C. It was thus billed as a systems language - but that's exactly what you don't want in a systems language. ALGOL is a pure algorithmic language, but was used as a very secure systems language in the B5000 and descendants - with it you could not blast your legs away. C++ is even worse, a pretend OO preprocessor where you can blow away the lower half of your body.

You skipped over Eiffel to Spark, which I had a quick look at, but I think Eiffel demands a more prominent mention as being the embodiment of DbC and thus Hoare's {P} S {R} paradigm.


Unfourtunately the last decades has been devoted to writing code in undetectable error languages. That's the bottom line here, even Java itself isn't a technically safe and sound language, so good luck with unsafe langs, the rest of us can use Modula-3


NaN is equivalent to a null; so what you want is to be able to interchange Integer objects with int primitives.

I would take design-by-contract even farther, and say that the method (or object) signature should be the contract. The more strongly typed the language, the more strict the contract.

Where the specification can't fit into the method signature, it should be written as a unit test. Hence the trend toward unit test domain specific languages, which make the test read like a specification.

If you have separate code and specification, there's redundancy, and bugs can creep into the specification just as easily as the code. Future of programming languages will be better at finding the middle ground between tedious specificity and easy-to-read ambiguity.

For example, Scala is extremely specific in its type system, which also makes it extremely complicated. I like to say it's a read-only language: once you've managed to get it to compile, it usually does the right thing.

Post-Scala languages, such as Kotlin, try to cram in all the best features of Scala while making the code more approachable.


You've given up too soon on C++.

Take a look at C++ libraries as rendered at, You'll find (more less) the following,

a) A large group of libraries based on a "functional model". i.e. less side effects which make library components easier to compose correctly.

b) template base code which permits algorithms to be decoupled from types. This diminishes the "brain surface area" to be more efficiently used. That is, understanding the usage of the library for one type of argument means that one understands it for all types of arguments,

c) b) above means less lines of code required. This makes it easier to actually finish a project. My experience is that re-factoring a (purportedly) working program in terms of modern C++ and Boost libraries typically cuts lines if code by a factor of 3.

d) Boost libraries include a test suite that you can compile and run yourself to verify that library code works as advertised in your environment. Tests on widely used compilers are run dailey and results can be consulted as needed. Also examining test code is often helpful to understanding any arcane details of how a library is to be used.

e) Boost libraries have documentation. 'nuff said.

f) many/most boost libraries implement compile time checking of template arguments (aka concepts). This makes the library functions harder to use wrong. Extra effort required to get one's program to compile is rewarded 10 fold in reduction of debugging time and surprises in "easier to use" languages,

g) using Boost encourages the implementation of unit testing in one's own projects to save time. (sometimes one has to do this on the QT to stem complaints from management about "wasting time" - oh well).

h) using unit testing encourages programming in terms of more composable, decoupled components which makes programming faster and easier.

Note that using more modern C++ and Boost does require some investment of effort. But this investment will payoff much better dividends than looking for a new language!

Looking for a new language won't help you. If you want to make correct programs, you have to approach the problem more formally.

Good luck on your quest though.

Robert Ramey


I think that the core of the problem is that most businesses (and in fact several companies that I have worked for in the past) have the mindset that the additional time involved is too expensive. The real problem is not that the language can't provide for more correctness, the problem is that the programmers are not given the time to implement said correctness.

In the end, the bugs cost us all more than the initial development would have, and in some cases cost the entire system way more than an extra couple of days would have originally taken (a la Knight Capital).


Years ago, in the UK, Occam was developed by Inmos and the Oxford Programming Group. The language was not a willy-nilly combo of features, but an algebraically checkable set of operations.

It was so good that chips were designed using this language - from high level language to chip masks - one smooth production flow.

It didn't catch on as a general programming language, even though it had explicit parallelism built-in. Too far ahead of its time.

The company Inmos was eventually bought-merged into STMicroelectronics, the Italian chip maker. I fantasize that STM's success is due in part to their internal design expertise using Occam.