[Jweb_Guru]

> At least, I didn't see in the "rustbelt" list of papers anything which appeared to indicate that a verified compiler or language subset do in fact exist.

You might want to look harder, because there is certainly a verified language subset (anything that can be written as LambdaRust, which covers a large and substantial swathe of the language).

If you're looking for a formally verified, optimizing compiler for any realistic language, particularly a low level language, you have pretty much one option: CompCert (I'm not sure where this large group of verified compilers you claim exists lives, but I'd love to see them). As someone who would love a verified Rust toolchain, I can't help but notice that very few safety-critical systems actually use CompCert in practice, which makes me a bit suspicious of claims that this is something Rust needs to be competitive in this arena.

Finally, I'll point out that verified compilers like CompCert only promise to translate correct C to correct machine code; they do not necessarily aid you in coming up with correct C in the first place. Miscompilations certainly happen, but not nearly as often as undefined behavior in the source program. So asking why people would use Rust when verified compilers exist for other languages is sort of missing the point.

[grumblenum]

I think Compcert isn’t widely used because of its license. GNAT is also GPL. Everyone lost their mind over Oracle charging a nominal sum for their compiler. I don’t think rust would have its corporate backing if it had similar licensing.

Also, there is only undefined behavior in rust. The compilers behavior can change at any time for any reason any time somebody with commit rights thinks that it should. You cannot begin to assert provenance about some thing that can change at any time.

[Jweb_Guru]

> I think Compcert isn’t widely used because of its license.

I somewhat doubt this, but even if it is true, the fact remains that people are not actually using it for the vast majority of mission-critical software. This suggests that the elimination of miscompilation bugs, which is what you get from formal verification of a compiler, is not high on their list of priorities.

> Also, there is only undefined behavior in rust. The compilers behavior can change at any time for any reason any time somebody with commit rights thinks that it should.

This is certainly not true of Rust in any practical sense.

I am not saying Rust doesn't need a certified version of its compiler that people can legally rely on for stuff like this (as opposed to practically). I am saying that this objection has nothing to do with the existence of a formally verified compiler, which is also not in practice used to compile mission-critical C programs. I think you are confusing certification of a compiler for mission-critical software, with formal verification of the language's compiler, semantics (including type safety of the safe subset--a proof that would not go through for C as it explicitly unsafe), and standard library.