Since you contrast the two approaches you might be interested in learning that CompCert also uses translation validation in some part of the compiler (notably for register allocation), see Jean-Baptiste Tristan's papers with Xavier.