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?