[tom_mellior]

> This turned out to be a premature optimization, actually! The CakeML compiler did full functional correctness proofs for their register allocator and report that it wasn't significantly harder than Compcert's translation validation.

Not sure if you're saying that using a translation validation approach for register allocation was a premature optimization. But if that's what you're saying, you're wrong: The paper describing the register allocation validator explains that this replaced a register allocator in Coq that was proved directly. The validator approach is much smaller and simpler than this direct proof was. So it was an actual optimization after the fact.

It's possible that CakeML does it better, of course.

[neel_k]

That's interesting! I heard this from some CakeML people, who told me they decided to go with a full proof because it wasn't much more work for them. Maybe Compcert has a fancier register allocator architecture that benefits more from translation validation?

[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.)