We do have formally verifying C and C++ compilers already. cbmc and esbmc.