I'm going to be a little nitpicky here: > Definition. An expression is a symbol of sequence of symbols given some interpretation. > Definition. A language is c

I'm going to be a little nitpicky here: > Definition. An expression is a symbol of sequence of symbols given some interpretation. > Definition. A language is collection of expressions. I immediately reject these definition. A language is a subset of the free monoid over some alphabet [1]. This definition is widely used and the author changing the definition here is significant. Next, because the author requires that each expression be given an interpretation, the author conflates language (e.g. valid strings) with semantics (e.g. the interpretation of strings). > The result of this sequence of symbols is undefined in C. ... > Definition. Undefined behavior is the result of interpreting a non-expression. The author is mixing around a few definitions of "undefined behavior". Of course, C compilers will gladly compile programs containing expressions that are total nonsense. The resulting behavior of the program has no meaningful semantics but the program itself consists only of valid expressions. Because a program may contain expressions that exhibit UB when operating with standard definitions (e.g. the definitions of "expression" and "language" ubiquitously used when discussing programming languages and compilers) the proof is incorrect. The immediate implication of this result is that technically a C program with UB is free to modify itself non-deterministically and thereby prevent any existing proof system from predicting its behavior. However, definitions aren't really "right" or "wrong." The proof is otherwise sound. My critique is that real systems aren't built using the definitions the author uses and therefore the resulting theorem isn't really applicable in any practical circumstance. [1] https://en.wikipedia.org/wiki/Formal_language https://en.wikipedia.org/wiki/Formal_language