Yes, the pointer issues Ralf raises has implications about what operations Rust can make safe. An example Ralf posed to the safe transmute working group: a transmutation from a reference (i.e., a pointer with provenance) to one without (e.g., a "raw" pointer) or to a `usize` number cannot be safe. (Rust can safely provide these conversions via the `as` keyword, just not via the more general framework of transmutations).

More broadly: Rust is very sensitive to LLVM bugs that inadvertently generate UB. The longstanding issues with `noalias` optimizations is the prime example of this: https://stackoverflow.com/a/57259339/7501301

How could transmutation from a reference to a usize not be safe? Do you mean "and back"?

Yes, absolutely. https://github.com/rust-lang/rust/issues/28728 is probably the most famous bug here, but many I-unsound bugs are similar.

This would be the case even without this. Compilers are programs. Programs have bugs.

This isn't the first soundness/compilations bug, it won't be the last. This bug can be fixed, hopefully with some work this whole class of bugs can be made rarer. If you were relying on your safety guarantees to include a bug free compiler - rust isn't there yet and you should stop. If you're relying on a bug free happy path, rust is as close as any other language implementation (with one or two exceptions pointed out in sibling comments).

So, I mean, if you're arguing that C/C++ programmers are culturally less repulsed by bugs... you might be right about that. Other than that I think it's about the same scale for C/C++ and rust - a bug is a bug no matter what language you wrote it in.

The only fundamental implications I think it has is that maybe we need to put more of an emphasis on formalizing the memory model if we want to reduce the number of soundness bugs (something that a number of people are already doing some awesome work towards).

It’s enough of an issue for C at least that a fully formally verified compiler exists: https://en.m.wikipedia.org/wiki/CompCert . That is, there’s proof that its (limited) optimisation passes are correct.

There’s other approaches to assurance of compiled code too, such as seL4 which has proofs that the binary itself is correct, I believe.

Note that fuzzing CompCert has still found bugs in it - because the entire compiler actually isn't verified. They've extended the proof over time.

(Note that "formally verified" still does not mean "bug free", it just means it's a refinement of a proof that is also a program which can have bugs in it. And "formally" sounds like a weasel word.)

Yeah, there were some bugs in the frontend and I think one in the backend. But there were zero bugs in the optimization pipeline, which is where typically the most subtle bucks lurk.

For more details, see https://www.cs.utah.edu/~regehr/papers/pldi11-preprint.pdf

Ah, thanks for the clarification!