Does the first incompleteness theorem imply that any Turing complete programming language must have undefined behavior?

Question

If I understand correctly, the first incompleteness theorem says that any "effectively axiomatized" formal system which is consistent must contain theorems which are independent of the axioms. In other words, there are models of the system where the theorem is provably true and others where it's provably false.

This seems rather similar to how the results of code that include undefined behavior cannot be determined by the language specifications alone -- in order to say what will happen, we need information about which particular compiler is being used and possibly also what hardware system it's being run on (which of course is why it's best to avoid undefined behavior when possible).

It seems like the language specifications of a given programming language, such as C++, might be an example of an "effectively axiomatized" mathematical system, while the various implementations would represent various models of the system. And so programs containing undefined behavior would correspond to theorems independent of the axioms. Is that correct?

Or, perhaps another way to do put it is, are all Turing complete models of computation examples of formal systems to which the incompleteness theorems apply, and, if so, does that imply that programming languages that implement such models must have undefined behavior? That is, is undefined behavior a necessary result of the incompleteness theorems applying to all Turing complete models of computation?

Answer 1

No, it doesn't require that. These are two orthogonal issues. You can easily define a new programming language where you provide fully defined semantics for all operations; yet it can be Turing complete. For a concrete example, consider Bitwise Cycle Tag; it is Turing complete, and yet it has no undefined behavior, because the behavior is always fully defined in all circumstances.

Answer 2

Your intuition is incorrect. The analogies you're trying to draw are not there, even though it's understandable you would expect them.

Programming languages can be defined as formal systems, but they are of a different kind than logic. Gödel's incompleteness theorems do not apply to them, because the formal systems do not even incorporate first-order logic.

C++ is not such a language because its specification is written in English on a 1000 pages. That's an outdated way of specifying languages.

For a modern account you can have a look at several textbooks, such as Benjamin Pierce's "Type theories and programming languages" and Bob Harper's "Practical foundations of programming languages" (a PDF of an early version is available). Chapter 6 of the linked PDF explains things in detail, but briefly, there are two theorems which together give "no undefined behavior":

Preservation: If a program $p$ has type $T$ and it can make an execution step $p \mapsto p'$ then $p'$ has type $T$.

Progress: If a program $p$ has a type then it is either a value (final result), or it has an execution step $p \mapsto p'$.

What this says is that no well-type program will ever get stuck: either it is done (a value), or it has one more step.

Note that "undefined behavior" is not the same thing as "runs forever" (some of the other answers assumed that's what was meant).

Answer 3

The incompleteness theorem only applies to formal systems that can express a certain amount of arithmetic. In particular, they have to support statements of the form $\forall n\in\mathbb N. P(n)$, because the Gödel sentence has that form. If your formal system can only express statements of the form $P(n)$ for fixed $n$, then it's not Gödelizable and there is no obstacle to its being consistent and complete.

For example, if $P(n)$ is the proposition that some program has not halted after $n$ steps, $\forall n\in\mathbb N. P(n)$ is the proposition that it never halts, which may be undecidable—but even if it is, every particular $P(n)$ may be decidable.

If you want to take the position that a program's behavior is undefined if you can't determine whether it halts, then indeed a Turing-complete language must have undefined behavior, but that's stronger than the notion of well-definedness that's normally used in computer science.