[tatterdemalion]

Proving the correctness of unsafe code is totally different from what you talked about, which was composing different abstractions with unsafe internals together.

Users of safe Rust do not need to worry about whether the composition of two safe interfaces that use unsafe internally is safe unless one of those interfaces is incorrect. Your comment would suggest that users need to think about the untyped invariants of each library they use, but this is not correct, libraries are not allowed to rely on untyped invariants for the correctness of their safe APIs.

[klodolph]

The problem with talking about this subject is that "safe" and "unsafe" are overloaded terms in Rust, so I can understand why you think I was talking about something different.

Let R be arbitrary Rust code with no "unsafe" blocks. Let X and Y be libraries with "unsafe" blocks. You can prove that R + X is safe, and prove that R + Y is safe, but you haven't yet proven R + X + Y is safe. This is the hard part, because without an understanding of what property of X and Y individually makes R + X + Y + Z + ... safe, we don't have a good definition for what makes an interface "safe".

And this is what I mean when I say that this is not only a pedagogical problem.

[stouset]

You have restated your position, but it is still incorrect in the context of this discussion. Even your original statement of "R be[ing] arbitrary Rust code with no 'unsafe' blocks" is problematic: any Rust code is, very unavoidably, built upon a foundation of unsafe code. It has to be, because it's running on an "unsafe" processor. And yet, any safe Rust code in the core library (barring a safeness bug) is obviously safely composable with any other safe Rust code precisely because it obeys safety guarantees when transitioning from unsafe to safe. The fact that you can mistakenly conceive of Rust code that somehow avoids any internal unsafety simply reinforces how obvious this simple fact is.

But using your original problem statement, if R is safe and X and Y use unsafe code but do not expose any unsafe interfaces, then either R + X + Y is safe or one of [X, Y] has a safety bug and is inaccurately marking an unsafe interface as safe.

This is a generally unsolvable problem, and every other language has this problem as well; the difference being that in most other languages you're typically forced to write the unsafe code in C (where one has much greater variety of footguns available at their disposal). If I write a Ruby FFI wrapper for buggy C code whose interfaces bleed "unsafe" (from the perspective of the Ruby VM) behavior, then I am liable to experience crashes and memory corruption bugs. The only difference here is that Rust allows you to break the seal on the warranty without switching to a different language.

[klodolph]

> ...is obviously safely composable with any other safe Rust code precisely because it obeys safety guarantees when transitioning from unsafe to safe.

And what are those safety guarantees? This is the part where I see a lot of handwaving.

> ...either R + X + Y is safe or one of [X, Y] has a safety bug and is inaccurately marking an unsafe interface as safe.

Correct, but the problem is that we don't have a way to identify which library is incorrect without a definition for what a "safe interface" is. If R + X were unsafe or R + Y were unsafe we would have an easy answer to that question.

> This is a generally unsolvable problem...

The fact that the problem is unsolvable in general did not stop people from inventing the Rust language in the first place. The point of Rust is to solve this problem for a larger and more useful class of programs. Likewise, the research into defining what a "safe interface" is in Rust is important and useful research, e.g., RustBelt.

On a minor note, these kind of negative interactions with individual Rust community members have given me a bad impression of the Rust community as a whole.

[dbaupp]

> And what are those safety guarantees? This is the part where I see a lot of handwaving.

I think this is the contention: correct me if I'm wrong, but you're saying, that, in practice, the safety guarantees of Rust are currently too nebulous to be able to be enforced reliably, whereas most other people in this thread are, I think, visualising the "platonic Rust"/post-RustBelt Rust where the currently vague conditions for safety have been tweaked as needed and proved correct, treating the current situation more like a "just" bug (and the success of RustBelt so far hints that this isn't vapourware/imagination, there's significant concrete progress towards it).

That is to say, most people are talking about the potential of Rust's safety, whereas you're talking about the reality, right now. I think both positions are reasonable to think about, but it obviously leads to confusion when the positions aren't distinguished in a discussion. (I also think that most people would agree with you about Rust right now: there isn't a definite set of safety rules, so it can be hard to work out whether "edge-cases" are correct or not.)

[steveklabnik]

I think this is a good point, thank you. Will be remembering to tease this out in the future!

[steveklabnik]

> And what are those safety guarantees?

It is still that we are still working this out; this is what we're cooprating with academia on, formalizing the exact semantics. Such things take time.