[denotational]

> I don't remember where I read this, but I think there are some examples in practice where instead of proving the correctness of some optimizations of existing C compilers (which is a codebase that keeps evolving), there have been situations where the correctness was ensured using program equivalence checking.

This is what CompCert does (or at least did when I last looked inside CompCert) for register allocation; the graph colouring algorithm is unverified, but a verified validator is used to check the colouring is correct.

Whilst this is relatively straightforward for something like graph colouring, it is substantially more difficult for comparing the outputs of two different compilers, which I think is what you are suggesting here?

There was some work to do a translation validation for the entire RTL -> LTL pass of CompCert, but I'm not sure how much progress was made or if this is currently used.