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

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)?

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:

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

-
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):

-
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.

-
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 co

StackExchange Computer Science Q#72014, answer score: 6