[tom_mellior]

Maybe, but on the other hand maybe the CakeML developers have some proof techniques that the CompCert people didn't think of. I don't know.

For reference, my only knowledge of this point comes from the CC 2010 paper at https://xavierleroy.org/publi/validation-regalloc.pdf, which says in section 5: "From a proof engineering viewpoint, the validator is a success. Its mechanized proof of correctness is only 900 lines of Coq, which is quite small for a 350-line piece of code. (The typical ratio for Coq program proofs is 6 to 8 lines of proof per line of code.) In contrast, 4300 lines of Coq proof were needed to verify the register allocation and spilling passes of the original CompCert compiler. Even this earlier development used translation validation on a sub-problem: the George-Appel graph coloring algorithm was implemented directly in untrusted Caml code, then followed by a verified validator to check that the resulting as- signment is a valid coloring of the interference graph. Later, Blazy, Robillard and Appel conducted a Coq proof of the graph coloring algorithm [13]. This is a fairly large proof: in total, more than 10000 lines of proof are needed to com- pletely verify the original CompCert register allocation and spilling passes."

(And hence my statement above was also inaccurate in that the original CompCert was not fully directly proven. I had misremembered the details of this paragraph. The point still stands that the newer validation solution is simpler.)