What cannot be proven at compile-time about a computer program?

Question

Is there a Turing-Complete-ish programming language without runtime errors? Like segmentation faults, memory leaks, race conditions, deadlock/livelock/starvation, etc.? With strongly typed languages, the compiler can detect null pointer exceptions and refuse to compile code. How much can we statically check? Everything, or are there some things impossible to check?

Are there any language projects that are trying to do this (especially with concurrent and networked applications)?

---

EDIT:

I guess there are two sorts of behavior that I'm looking to avoid: unwanted erroneous behavior (deadlocks, etc), and runtime exceptions (divide-by-zero, etc).

Taking the example of divide-by-zero, can we create some computation x/y so that, whenever such a computation is done, we require y to be of the type T nonzero where T is integer, floating-point, or whatever for that overloaded operator?

With deadlocks, and other concurrent scheduling hazards, is there a set of control structures which cannot create those hazards, or better yet, can detect those hazards at compile time (better because I think it might be more expressive)?

Answer 1

In the theory of programming languages there are the so-called safety theorems which tell us that programs "do not do bad things". A typical safety theorem says:

Safety theorem: If a program $P$ has a type $T$, then it either runs forever or it terminates and yields a value of type $T$.

Not every language satisfies such a theorem, and in fact, it usually takes a bit of work to make sure that a language is safe. Once we have the theorem, the compiler can make a strong guarantee by checking that the program has a type.

The safety theorem guarantees that:

1. A program which has a type will never get stuck, i.e., it will not encounter an undefined state.

2. A program which has a type will not suddenly switch to doing something completely diffrerent, for instance, it will not return a string if its type is int.

What exactly this means in practice depends a lot on what sort of information is expressed by the types of the language. For example, since a well-typed program will not get stuck, we can be sure that it will not segfault, and it will not perform an invalid pointer dereference. This is quite useful to know. Many modern programming languages strive to provide this sort of guarantee, or actually have it in cases of programming languages that have formal definitions (SML).

There are other kinds of errors which we might try to prevent, for example division by zero. Since it is non-computable whether a particular operation will happen at runtime, we cannot expect that the compiler will simply figure out whether division by zero is possible. In order to recover the safety theorem in presence of division by zero we can introduce exceptions into the language and make sure that division by zero raises an exception (rather than encounters an undefined state). The safety theorem then says:

Safety theorem (with expcetions): If a program $P$ has type $T$, then it runs forever or terminates by either returning a value of type $T$ or raising an exception.

This sounds like cheating but is the best we can do with this sort of language. It is also a very common solution, also because exceptions are a generally useful programming concept (they are not errors, but rather a flow control mechanism). We can do slightly better if we allow the types to contain information about exceptions. Java does this with the throws declaration. Note however, that types cannot describe runtime exceptions exactly because that would make type checking non-computable.

Another way to deal with division by zero is to design the language in such a way that it is impossible to divide by zero. This could be accomplished by having a construct

x / y orelse z

which divides x by y if y is not zero, or returns z otherwise. Most programmers would find this kind of solution impractical.

Deadlock and race conditions are problematic in the same way as division by zero. In the general case it is non-computable whether a deadlock, or a race condition will happen. There are two lines of attack (just as with division by zero):

1. We can have more expressive types which guarantee that deadlock does not happen. The danger is that the types will be so fancy that type checking becomes undecidable, or that programmers will find the types too complex to understand.

2. We can design the language so that deadlock is impossible. The danger is that we will impoverish the language by doing so.

Regarding the second point above: programmers and designers of programming languages both like to use loss of expressivity as an excuse for a non-safe design. A case in point is the null pointer/object/value, where it is often falsely claimed that not having null is impractical and results in slower code. Good design goes a long way, and sometimes requires change of habits, but brings many many advantages. (It used to be the case that "real programmers" disliked garbage collection, and never admitted to themsleves that their programs leaked memory because humans could not allocate and deallocate memory by hand correctly).

In general, by making types even fancier, we can make sure that the safety theorem precludes other kinds of bad behavior by specifying good behavior. For example, in a dependently typed langauge such as Idris you can specify that your program sorts lists, in which case it can't cause division by zero, nor can it run forever. (But now the compiler may possibly need a lot of help from the programmer in order to establish that the program really has the stated type.)

You might expect also that a compiler shold be able to guarantee that a well-typed program must terminate. However, this is non-computable (Halting Oracle), not to mention that there are many useful possibly non-terminating programs (such as the browser you're using right now, and the operating system). If you need termination guarantees, then instead of referring to a safety theorem, you can design the language so that it cannot express a non-terminating computation. An example of such a language is Agda, which is also dependently typed and it doubles as a proof assistant. Note however that there is an important theorem stating that a language with computable syntax in which all programs terminate is not Turing complete.

Answer 2

Yes, there is a programming language without runtime errors. For instance, my programming language only lets you compute sums of numbers: valid programs include 2+2 and 3+17+42+19 but not anything more complicated (you can only have constants and the addition operator, but nothing more); all operations are done with big integers, so no runtime errors are possible.

However, as you can see, this language is extremely limited in what it can express.

The answer depends on what you mean by "runtime error", and on what kinds of operations you want the programming language to be able to support.

Let's start with what we mean by "runtime error". Here is my understanding. My impression is that deadlock, livelock, starvation, and infinite loops generally aren't considered runtime errors. Anything that causes the program to run forever without making useful progress is a failure of availability, but not of safety -- not a runtime error, as I understand the term. In contrast, segmentation faults, null pointer dereferences, etc. generally are considered runtime errors. They can cause the program to crash, go wrong, or return incorrect answers.

With that understanding, it is possible to make a language that is free of runtime errors, if you're willing to make enough compromises about what constructs are allowed in the language. We can define all the operations supported by language so that no runtime error is ever possible, and then we could have a language where you can guarantee absence of runtime errors. However, this might or might not be what you were actually hoping for. For instance, normally we define the division operator so that x/y is a runtime error if y is zero. That won't work. We could alternatively define a programming language where the result of x/y is defined to be something specific (zero; NaN) if y is zero. Thus / doesn't represent the usual division operator; it represents something slightly different. We could continue to do the same for every operation that might cause a runtime error.

In this way, you could obtain a language with no runtime errors. However, you'll have to decide whether you like the result or not -- it has a somewhat different flavor from many imperative languages you might be used to. For instance, imagine a language like Python, except surrounded by a giant try-catch block that ensures if any runtime error occurs at runtime, the program terminates and returns 0 -- that would be fully defined and have no runtime errors, but only by virtue of "re-defining" the meaning of runtime error to mean that we don't count it as a runtime error (even though it's probably still a bad thing if a program tries to divide by zero).

Suppose you don't like that outcome, and you really want a language where you can determine that a program will never cause any runtime error, including never attempt to divide by zero. Unfortunately, I have bad news. It is not possible to have a programming language with that property, and that is also fully expressive. In particular, if it is Turing-complete programming language, and if it supports the division operator, it can't be guaranteed free of runtime errors, because determining whether a divide-by-zero error can occur at runtime is as hard as the halting problem and thus undecidable. The same occurs for every other operator that could potentially trigger a runtime error.

As a result, if you are imagining a language that looks like typical imperative programming languages, the pragmatic answer to your question is going to be "no: you can't have a language with that property (if you want it to be Turing-complete and to feel familiar), because deciding whether or not a program will cause a runtime error is undecidable".