What are the conditions necessary for a programming language to have no undefined behavior?

Question

For context, yesterday I posted Does the first incompleteness theorem imply that any Turing complete programming language must have undefined behavior?. Part of what prompted me to ask that question in the first place is that, awhile ago, someone on the learnprogramming subreddit told me something about the reason C++ in particular having so much undefined behavior is because, for it to not have undefined behavior, it would have to use a much more restrictive language model, but they didn't explain what that means exactly. I had also asked on Quora awhile ago about why C++ compilers don't always throw errors when a program contains undefined behavior and at least one answer mentioned something about it being fundamentally impossible to always detect undefined behavior at compile time and that this was related to the halting problem being undecidable.

Those two things combined have me wondering about models of computing more generally -- my understanding is that all/most popular programming languages, including C++, are Turing complete, and since I was told the problem of detecting UB in C++ is fundamental and related to the halting problem, I thought that perhaps all Turing complete programming languages must have undefined behavior and C++ is just worse at hiding it than others. But judging from the answers to my above-linked question, I was mistaken about that.

So my question now is, what conditions need to be imposed on a Turing complete language in order to guarantee that all possible programs written in the language will have fully defined behavior determined by the language specification? And, on a side note, does the answer have anything to do with the incompleteness theorems? I ask the latter question because the idea of defining a language for which all possible programs have fully defined behavior seems quite similar to the idea of defining an axiom system for which all possible theorems are provable/disprovable.

Answer 1

The problem of statically detecting undefined behavior has nothing to do with undefinedness as such. It's just impossible to prove in general that programs in a Turing-complete language will do anything (Rice's theorem). For example, if your main function looks like

int main() {
    do_something();
    cout << "Done" << endl;
}

then for any algorithm attempting to determine whether the program halts, there is some definition of do_something that will fool it. For the same reason, for any algorithm attempting to determine whether the program displays Done, there is a definition of do_something that will fool it. For the same reason, if you add "42"[42]; at the end, then for any compiler that tries to warn you about undefined behavior, there is a definition of do_something that will fool it.

Whether a program displays Done is decidable for a Turing-complete language that has no way to display text. Likewise, whether a program has undefined behavior is decidable for a Turing-complete language that completely defines the behavior of every program (as Turing's original computing model did, for instance).

It is possible to detect and warn about undefined behavior in C++ in many cases, and popular compilers could do a better job of it than they do.

someone [...] told me [...] for [C++] to not have undefined behavior it would have to use a much more restrictive language model, but they didn't explain what that meant exactly.

They probably meant that defining the behavior of every program makes optimization more difficult. For example, if the effect of an out-of-bounds array access is defined, then every array access has to be compiled into code that checks whether the index is out of bounds so it can do the mandated thing (unless the compiler can prove that that code is dead, which in many cases is not possible). If the effect is not defined then the compiler can just generate a single memory-access instruction. It may crash the program, or overwrite some other variable causing weird, hard-to-debug behavior down the line, but that's okay, because that can only happen when the index was out of bounds, and the spec says anything goes then.

Answer 2

First off, let's be clear on what "undefined behaviour" is. In just C alone (and this is the understanding inherited by C++), there are two possible meanings, depending on which version of the standard you choose.

The C89 standard, section 3.16, defines:

undefined behavior: Behavior, upon use of a nonportable or erroneous program construct, or of erroneous data, or of indeterminately-valued objects, for which this International Standard imposes no requirements. Permissible undefined behavior ranges from ignoring the situation completely with unpredictable results, to behaving during translation or program execution in a documented manner characteristic of the environment (with or without the issuance of a diagnostic message), to terminating a translation or execution (with the issuance of a diagnostic message).

The 1999 C Rationale explains:

Undefined behavior gives the implementor license not to catch certain program errors that are difficult to diagnose. It also identifies areas of possible conforming language extension: the implementor may augment the language by providing a definition of the officially undefined behavior.

The C99 standard, section 3.4.3, words it slightly differently, turning the second sentence into an explanatory note:

undefined behavior behavior, upon use of a nonportable or erroneous program construct or of erroneous data, for which this International Standard imposes no requirements

NOTE Possible undefined behavior ranges from ignoring the situation completely with unpredictable results, to behaving during translation or program execution in a documented manner characteristic of the environment (with or without the issuance of a diagnostic message), to terminating a translation or execution (with the issuance of a diagnostic message).

EXAMPLE An example of undefined behavior is the behavior on integer overflow.

Note that in the second sentence, the word "permissible" was changed to the word "possible".

The way everyone interpreted the C89 standard was that the second sentence was normative: it described the set of permissible behaviours. So "undefined behaviour" is only "undefined" in the sense that the standard does not require which of the permissible behaviours an implementation may do.

But with C99, following ISO rules, moving the second sentence to an explanatory note and changing the word "permissible" to "possible" means that it is not normative. These are merely possible behaviours, but because the standard imposes no requirements, any behaviour is possible. This is sometimes jokingly known as a nasal demon, because making demons fly out of your nose is a possible behaviour.

This is more than a little controversial, and the reinterpretation has caused customary C programming idioms to become bugs, including one in SPECint, the standard suite of integer benchmarks. Chris Lattner of LLVM put it this way: "huge bodies of C code are land mines just waiting to explode."

But I digress.

C is designed as a systems programming language, and as such, allowing direct manipulation of the underlying platform (e.g. CPU, OS) is a feature. But C is also meant to be portable, which means that differences in the underlying platform manifest as differences in behaviour of the program. And sometimes, this behaviour is a global property of the program, not detectable in any specific line of code.

There are essentially only three ways out of this, for any given situation that would otherwise be undefined behaviour.

1. Define the behaviour. For example, you could mandate two's complement arithmetic so that integer overflow has a defined behaviour. In some situations this may require extra code; see point 3. For example, shifting a 64-bit word left by 64 bits might seem to have a reasonable "answer" (i.e. zero), but the shift left instruction on many CPUs doesn't do this, so this would require extra code to detect it.
2. Provide enough static guarantees such that UB never occurs. This could be anything from not having language support for the kind of activity that might cause UB (e.g. unsafe references or pointer arithmetic, which many languages simply don't have) to having a strong static type system which the programmer cannot subvert (e.g. to disallow modifying static strings).
3. Generate code to detect the situation at run-time and take action then (e.g. raise an exception, terminate the program, substitute defined behaviour).

Answer 3

The C language may say "if you do X, then whatever the result is, is not a violation of the C Standard". "Whatever the result is" can include the result that you hoped for, some completely different result, your software crashing, or your program doing strange things. An example for this would be to write

int a[2]; const int b = 3; a[2] = 5;

which is undefined behaviour, and the result might be that now b is 5. But not always. So printing b twice could print 5 and 3. And quite often "whatever the result is" includes "nothing bad happens when the developer runs the software, but as soon as it is delivered to a customer, all hell breaks lose".

How can the language eliminate undefined behaviour? It must define the behaviour of any code that you execute. It may include "your program crashes" as a possible behaviour. For example, Swift does that in many situation. If you access the data in a nil object, the program crashes. It crashes definitely (unlike C where it may crash or do nothing or do something worse than crashing).

The compiler must enforce this. So it may add code that checks for unusual situations (situations that would be undefined behaviour in C). Or it may set up things so that a crash happens automatically with checks done for free in the computer's hardware. Or it may prove that an unusual situation cannot happen. As an example, in a loop for (i = 0; i < limit; ++i) you can prove that the ++i cannot produce an arithmetic overflow if i is not modified elsewhere. So this increment can be executed without checking for an overflow.

Another possibility is to just define the behaviour. For example, shifting a 64 bit integer x to the left by 64 bit positions is undefined behaviour in C. The "natural" hardware instruction that shifts by arbitrary amounts will leave x unchanged on a 64 bit Intel processor, and set it to 0 on an ARM processor. So you could have a language "C for Intel" that has the defined behaviour that x << 64 produces the result x, and another language "C for ARM" that has the defined behaviour that x << 64 produces the result 0. Whether this is useful is another question, because using x << 64 is not portable code.

Answer 4

So my question now is, what conditions need to be imposed on a Turing complete language in order to guarantee that all possible programs written in the language will have fully defined behavior determined by the language specification?

1. Enough time and attention to specify all possible behaviors in all corner cases
2. Either no multi-threading at all, or a will to do something similar to Python's GIL (Global Interpreter Lock).

Although one can argue that a good memory model is not "undefined behavior" even if there is no global lock, I think it's still worth mentioning.

E.g. Java/Kotlin/Scala have no undefined behavior in C/C++ sense except for some dark corners of multi-threading that I'm not sure about. Maybe the deprecated Thread.stop().

And, on a side note, does the answer have anything to do with the incompleteness theorems? I ask the latter question because the idea of defining a language for which all possible programs have fully defined behavior seems quite similar to the idea of defining an axiom system for which all possible theorems are provable/disprovable.

Absolutely not. A program is more similar to "expression" rather than "theorem". You execute program to obtain a result, step-by-step, and everything goes well as long as all steps are precisely defined.

What you will have troubles with is theorems about programs. E.g. "can this integer overflow ever happen". That is impossible to determine in general. So you cannot rely on a "smart compiler" to eliminate undefined behavior, you have to eliminate it in the language's specification and define all possible behavior, no matter how unlikely it seems.

Answer 5

Lets look at a sample program

Collatz_thingy(bigint n):
seen = set()
While not n in seen:
   seen.add(n)
   If n odd:
       n = 3n + 1
   Else:
       n = n / 2
N_64 = Cast(n, int64)
result = new char[5]
result[N_64] = ‘x’
Return result `

In a language with no undefined behavior, the compiler has to either insert a bounds check in result[N_64] = ‘x’ , prove the collatz conjecture, or refuse to compile unless you provide a proof of the collatz conjecture in a type annotation. The authors of C and C++ are incredibly averse to automatic insertion of bounds checks.

Answer 6

Starting from the C/C++ languages, ruling out all undefined behavior would be very hard. But if you're designing a language from scratch, it's not difficult at all to rule out undefined behavior. Many languages -- including type-safe compiled languages, and typically interpreted/dynamic languages -- have no such thing as undefined behavior*. There may be cases where they will reject a program as invalid, or cases where they run a program and it crashes (because the semantics of the language call for it to crash.) But there's no need for them to have cases where a program's behavior is not defined by the language.

(*Many otherwise-safe languages have various features which are clearly documented as being unsafe, and inherently cannot be otherwise by their nature. This includes things like foreign-function interfaces, through which you can call C code, for example. I think it's fair to say a language "does not have undefined behavior" if you can avoid it by avoiding those features. I also don't count compiler bugs, for obvious reasons, even though those can result in a safe language displaying unsafe behavior.)

Incompleteness is most often irrelevant in practice, and I claim it is irrelevant here. One could maybe use it to show that, in a sufficiently powerful language, some hypothetically safe programs cannot be proven safe. But that doesn't actually matter. In practice, it's easy to design a language where the programs we actually wish to write can be proven safe. And then we can simply reject all other programs.

In proof theory terms, you should think of every program as (ideally) coming with a proof of safety -- a proof that the program executes correctly and has defined behavior. In C/C++, the type system is supposed to provide that proof, but it's kind of leaky. You can write a program which passes type checking, but does not actually have well-defined behavior.

But in, say, Haskell or OCaml (if you refrain from using deliberately-unsafe features), the proof system is sound -- the type checker only accepts programs which have well-defined behavior. And in something like Python (again, if you refrain from deliberately using unsafe features), the semantics of the language are such that you don't need a type checker to ensure well-defined behavior, because you instead have runtime safety checks on every operation that could fail. This is slower, but much easier to engineer.

Answer 7

I would argue that there is one very specific requirement to defeat undefined behaviour: that the programming language designers control the hardware design.

Undefined behaviour exists notionally to allow variation in compiler implementation, but that is desirable primarily when different compilers target different hardware, each themselves with somewhat different (or even very different) conceptions and architectures.

These different hardware architectures prevent the language having a defined behaviour in certain corners, because what is a reasonable implementation on one architecture may be unacceptably inefficient on another.

So undefined behaviour is the result of disintegrated design.

Many languages like C still date from an era when microprocessor designs were more various for real technical and creative reasons, and high-level languages (as C was then) sought to find the common ground between them.

Nowadays, it's all just legacy, and simpler and more consistent integrated designs are prevented only because of heavy transition costs, and because the total costs of undefined behaviour are mostly sunk (with only a small ongoing cost).