Summary
An unprovable error is one that no amount of testing can ever be assured of revealing. With computers becoming more networked and security becoming more important, should we be thinking about how our programming tools can avoid unprovable errors?

Consider the following C program:

#include <assert.h>

int x = 0;

int incr() { ++x; return 0; }
int decr() { assert (x > 0); --x; return 0; }

int main()
{
    incr() + decr();
    return 0;
}

Whether this program runs or trips the assert depends on the order in which the implementation calls incr and decr. If the implementation happens to call incr first, the program will succeed; otherwise it will fail.

Consider the problem of finding this error if all you have is a C implementation that always evaluates the left-hand side of an addition first. The only way that testing will reveal the problem is if you run the program on a different implementation.

This is a small example of a larger problem: Some errors simply cannot be detected by testing because language definitions and implementations give enough leeway that it might always be possible to get the "right" result by coincidence. When a program with such an error is run on another implementation, the error might become serious.

I propose to call such errors unprovable errors. This coinage is by analogy with Goedel's Theorem, which says that any consistent logical system will have statements that are true but cannot be proved within the system. Analogously, it is possible for any programming language (at least any I know) to allow programs with errors that no amount of testing can be assured of revealing.

Pragmatically, some languages make it much harder to write such programs than others. A useful property for such a language is to assure that programs will run exactly the same way on all implementations, and to assure also that the implementation will detect a program that does something that the language definition does not allow. If you like, anything that language definitions refer to as "undefined behavior" is an example of an unprovable error.

I would like readers to wonder out loud along with me about what it might be possible to do about designs of future programming languages and tools to make unprovable errors less common.

Talk Back!

Have an opinion? Readers have already posted 19 comments about this weblog entry. Why not add yours?

RSS Feed

If you'd like to be notified whenever Andrew Koenig adds a new entry to his weblog, subscribe to his RSS feed.

Digg | del.icio.us | Reddit

About the Blogger

In his 35+ years as a programmer, Andrew Koenig has written an online student registration system in APL, a software distribution system in a mixture of C and C++, pattern matching libraries in C++, ML, and Python, and a compiler for a syntactically sweetened front-end for Snobol4 in its own language. He has published more than 150 articles, and is author or coauthor of three books "C Traps and Pitfalls,'' "Ruminations on C++,'' and "Accelerated C++.'' He believes that he was the first person to write an efficient associative-array library in C++, and also the first to port the Adventure game to C.