You don't really need compilers anymore. LLM's can write programs over any AST and provide an equivalence proof provided you have good semantics for the source and target.
I was mostly referring to accuracy when I said "good" above, in the sense that they should reflect the actual behaviour of the language they describe.
/s