All compilers have miscompilation bugs. Even ones that are proven correct.
> has no specifications or alternative implementations, right?
There is one alternative implementation that is good enough to bitwise reproduce rustc, there are a few other in-progress alternate implementations.
> I’m not aware of any progress in “sealed rust” or “rust belt”
That doesn't mean they haven't progressed. By the way, "Sealed Rust" is now called "Ferrocene" and is expected to GA in late 2022. https://ferrous-systems.com/ferrocene/
> There are other verified compilers that could be used now, though.
This is true, for sure. A compiler being verified is not a panacea.
The stated goal of the grant program is to rewrite stable software many people use in Rust with the implied context being that C can’t be trusted, but Rust can be. I’m surprised that a language with no specified guarantees is favored over well established methods of verification. When you poopoo formal methods and verified compilers, it’s very hard to find a coherent logic behind RIIR, which offers much less in terms of security.
Unless the exercise is a pretext to rationalize the grant money (which would be the real purpose).
The formal verification researchers I've worked with love Rust, because its type system nails the basics so they can focus on proving more interesting properties.
Rust and formal verification work really well together. You can formally verify properties in a small section of critical code, then use the type and lifetime systems to expand those properties to the whole codebase. It's not an either/or, it's a both/and.
All compilers have miscompilation bugs. Even ones that are proven correct.
> has no specifications or alternative implementations, right?
There is one alternative implementation that is good enough to bitwise reproduce rustc, there are a few other in-progress alternate implementations.
> I’m not aware of any progress in “sealed rust” or “rust belt”
That doesn't mean they haven't progressed. By the way, "Sealed Rust" is now called "Ferrocene" and is expected to GA in late 2022. https://ferrous-systems.com/ferrocene/
> There are other verified compilers that could be used now, though.
This is true, for sure. A compiler being verified is not a panacea.