Proof of the undecidability of compiler code optimization

While reading Compilers by Alfred Aho, I came across this statement:

The problem of generating the
optimal target code from a source program is undecidable in general.

The Wikipedia entry on optimizing compilers reiterates the same without a proof.

Here's my question: Is there a proof (formal or informal) of why this statement is true? If so, please provide it.

Optimized program must have the same behavior as the original program. Consider the following program:

int main() {
    f();
    g();
}

, where it's guaranteed that $f$ is pure function. The only question is: does it finish its execution? If it does, then we can replace main()'s body with g(). Otherwise, we should replace it with an infinite loop. Unfortunately, verifying whether f() finishes its execution is undecidable.

Another example is the program with body print(f(42)), where f is pure. The optimal program would just replace f(42) with its value. However, there is no algorithm that does this. We may try to compute it in compile-time, but it may never finish.

Another example (now without infinite loops). Assume that your program defines a context-free grammar and $f(x)$ checks whether string $x$ belongs to the language defined by this grammar (for any CFG we can build such $f$ automatically). Then if $f$ is a constant "true", then

if (f(x)) {
    g()
}

can be optimized to g(). Unfortunately, checking that grammar accepts all strings is called a universality problem and is known to be undecidable.

StackExchange Computer Science Q#128604, answer score: 42