Comment by afdbcreid

There is a severe misunderstanding here. Beside being only a subset, CompCert definitely has UB. It just formalizes codegen for codebases not containing UB, which obviously won't be enough for Rust.