[rkangel]

> I've never read anything to make me think that Rust is a safer alternative than any of these options; the guarantees of the language are just assurances of its advocates.

Note that some formal verification work has been done on the guarantees that the borrow checked provides (which led to finding and fixing an edge case bug), so there is a little more concrete evidence that just the "assurances of its advocates"

See http://plv.mpi-sws.org/rustbelt/ for more information, also the verification working group: https://rust-lang-nursery.github.io/wg-verification/

[grumblenum]

I don't think that the mere existence of a "working group" or grant funded research positions for verifying rustc or a subset thereof is the same as having a verified compiler. That's certainly not a strong argument to against using rustc for safety over one of the many verified compilers that actually exist. 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. Furthermore, that the proposed patches rely on the nightly compiler and a special variant of rust's core, which can only be enforced by special feature tags seems to suggest that Rust-Linux is not being written in this hypothetical, future compiler.

[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.

[steveklabnik]

It has not been done yet, it is a work in progress, but it is being done. https://ferrous-systems.com/blog/sealed-rust-the-pitch/

[grumblenum]

My point is that solicitations for grant money do not provide the assurance that products that actually exist do.

[steveklabnik]

Sure, I am here to state the current state of the world and point to the most up-to-date way to find out what the status is, that's it.

[gnzoidberg]

So... it hasn't been done

[steveklabnik]

That is what I said, yes.

(Though, as pointed out by a sibling, there is a subset that is.)