Pre-RFC: Unsafe Types

I’m sorry I have to get into this discussion, even if it is somewhat off-topic :wink:

I absolutely agree with @Gankra here, there is a fundamental difference between “trusting the rest of the universe” and “trusting your own implementation”. This difference is pretty clear when it comes to proving stuff.

Right now, when I want to prove Vec correct - where correct means “no safe clients can cause crashes or data races” - then I will consider the entire module Vec is defined in. I assume the rest of the world to be some (safe!) Rust program that does just about whatever it wants with my module. I can now prove that Vec is correct, because I know all the code that ever touches len, and can verify that every such access maintains the invariant. This is possible right now even though there is no such thing as an unsafe field, because len is private.

Now, let’s try to prove that spawn is correct, and lets assume we look at the entire libstd. Again we assume that the rest of the world (i.e., everything outside libstd), calling us, is some safe Rust program. Because it is a safe program, I know it does not contain any implementation of Send or Sync. I can thus prove that there will be no data-races, since I know all the types in libstd actually are thread-safe. (Really, rather than considering the entire libstd at once, one will first try to figure out what Send and Sync actually concretely promise to the rest of the world, and then prove this locally for every implementation, while relying on it in every consumer.)

Now, if you take away unsafe traits - there is just no way to have spawn. Note that we crucially relied above on the fact that the safe Rust program calling us does not implement Send or Sync. Without unsafe traits, we cannot make such an assumption. We would either have to remove spawn from libstd, or give up on our goal of having a “correct” libstd in the sense that safe code can cause no havoc (in other words, we’d be in C++).

So: Unsafe traits are needed to fulfill Rust’s promise of safety with respect to an arbitrary, safe client. Unsafe fields are not.

5 Likes

I’ve started to feel pretty strongly that we ought to have unsafe fields (not types). This is based on some recent experience trying to better document unsafety in rayon. Basically, I am trying to be systematic about labeling the assumptions that (e.g.) an unsafe fn requires of its caller as well as, in the case of unsafe blocks, labelling the assumptions within. To this end, I found it pretty helpful to have the compiler guiding me to the places I needed to check (and document) assumptions.

One thing I noticed though was that modifications to unsafe fields, which might violate the invariants I was trying to label, were not caught (duh) and hence it was easy to overlook them. This, combined with the fact that it provides an obvious hook for documentation (“this field is unsafe because you must maintain invariant blah”), seems like an overall win in my book.

3 Likes

Unsafe fields could be (mostly) emulated without compiler support by a newtype with a private value and a setter and a getter which are both unsafe. So as a first step to evaluate the usefulness, we could simply add an unstable UnsafeWrapper type to libstd.

Of course this doesn’t give the full guarantees of an unsafe field, since you can swap two fields of type UnsafeWrapper without any problems, but it should catch most usages.

Playground

Niko, I’m not sure if you followed https://github.com/rust-lang/rfcs/issues/381#issuecomment-174651558 which is where a lot of discussion has been happening recently.

Thanks for the tip. :slightly_smiling:

What is the relation of this Pre-RFC and dependent types? Can’t that be used instead? If not - what effect would it have in conjunction with full dependent types?

I… don’t see any relation to be honest. Or are you suggesting that we embed an interactive theorem prover in Rust and have people prove that their unsafe code upholds the invariants they specified for their type? That seems… rather far-fetched, to say the least. :wink:

I believe unsafe types/fields and dependent types are totally unrelated in terms of their syntax, semantics and implementation. But there is some overlap in the use cases these features target (both might help with the len <= capacity invariant, for instance), which I’m guessing is what @Centril was getting at.

See also https://github.com/rust-lang/rfcs/issues/381#issuecomment-175120933 in which @Gankra says “Really, it seems to me that we all just want dependent types and/or design-by-contract invariants/constraints. All this unsafe field/type stuff is just a horribly poor version of those features.”

1 Like

This topic was automatically closed 90 days after the last reply. New replies are no longer allowed.