> And C is also AFAIK the only language with a formally proven compiler CompCert C.

There's CakeML, which is a formally verified subset of Standard ML [0]

[0]: https://cakeml.org/popl14.pdf

CompCert doesn't stop you from writing memory unsafe C, of course, just that it won't miscompile your maybe memory unsafe C.

curiously, seL4 doesn't need to trust the compiler: the assembly is verified to satisfy the abstract specification