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.

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

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