-We can perform the optimization, *we just cannot perform it in C*.
-Instead, we have to perform it in LLVM IR (or any other IR with a suitable semantics).
-Specifically, signed integer overflow in LLVM yields a `poison` result.
-It is not UB to produce `poison`, it is just UB to use `poison` in certain ways (the details do not matter here).
-In a call to `sum_up(INT_MAX, 1, 0)`, the `s` variable introduced by loop hoisting is unused, so the fact that its value is `poison` does not matter!
-
-Due to this behavior of signed integer overflow, the loop hoisting optimization is *correct* if we consider it as an optimization on programs that are written in LLVM IR.[^cheat]
-In particular, this means we can freely combine this optimization with any other optimization that is *correct* in LLVM IR (such as inlining, replacing definite UB by `unreachable`, and removing unreachable code), and we can be sure that the result obtained after all these optimizations is a correct compilation of our original program.
-
-However, to make the argument that an optimization is *correct*, the exact semantics of LLVM IR (what the behavior of all possible programs is and when they have UB) needs to be precisely and unambiguously documented.
-All involved optimizations need to exactly agree on what is and is not UB, to ensure that whatever code they produce will not be considered UB by a later optimization.[^ub-difference]
-This is exactly what we also expect from the specification of a programming language such as C, which is why I think we should consider compiler IRs as proper programming languages in their own right, and specify them with the same diligence as we would specify "normal" languages.
+So far, what we have seen is that the optimization is not *correct* when being performed on a C program.
+But when LLVM performs these optimizations, it does not consider the program to be written in C---it considers the program to be written in LLVM IR, which has a different semantics than C.
+Specifically, signed integer overflow in LLVM IR yields a `poison` result.
+It is not UB to produce `poison`, it is just UB to use `poison` in certain ways (the details of this do not matter here).
+In a call to the optimized `sum_up(INT_MAX, 1, 0)`, the `s` variable introduced by loop-invariant code motion is unused, so the fact that its value is `poison` does not matter!
+
+Due to this behavior of signed integer overflow, this case of loop-invariant code motion is *correct* if we consider it as an optimization on programs that are written in LLVM IR.[^cheat]
+The "price" we pay for this is that replacing `INT_MAX+1` by `unreachable` is not *correct* in LLVM IR, since it is not UB.
+
+The great thing about *correct* optimizations is that we can combine any number of them in any order (such as inlining, replacing definite UB by `unreachable`, and removing unreachable code), and we can be sure that the result obtained after all these optimizations is a correct compilation of our original program.
+(In the academic lingo, we would say that "refinement is transitive".)
+
+However, to make the argument that an optimization is *correct*, the exact semantics of LLVM IR (what the behavior of all possible programs is and when they have UB) needs to be documented.
+All involved optimizations need to exactly agree on what is and is not UB, to ensure that whatever code they produce will not be considered UB by a later optimization.
+This is exactly what we also expect from the specification of a programming language such as C, which is why I think we should consider compiler IRs as proper programming languages in their own right, and specify them with the same diligence as we would specify "normal" languages.[^ub-difference]