5 ms·

Using unsafe is like providing a "proof" that the code you write won't cause safe Rust to exhibit undefined behavior. Writing unsafe requires a certain degree

Using unsafe is like providing a "proof" that the code you write won't cause safe Rust to exhibit undefined behavior. Writing unsafe requires a certain degree of skill, because one needs a deep understanding about what guarantees safe Rust provides, to ensure that your abstraction does not break them. If you read the standard library docs, every unsafe block has a comment explaining / proving why it can't cause safe Rust code to exhibit undefined behavior. Many of these blocks, particularly those in libcore, have been proved formally correct in proof assistants. There is a theorem that proves that "if a safe Rust wrapper over unsafe code is proven correct, then extending safe Rust with that wrapper is still sound". So you basically can infinitely extend the safe Rust subset of Rust with these abstractions. > But if “unsafe” is used, can we still claim that Rust code is safe? So the answer to this is "no, you can't claim that, you have to actually go and prove it". Often, very often actually, the proofs are trivial. For example, to index into a slice: fn index_slice(slice: &[T], i: usize) // SAFETY: if the index is not in bounds, we panic assert!(i < slice.len()); unsafe { *slice.as_ptr().add(i) } } suffices. Why? Because code that creates a slice with a ptr and a len field that do not point to a valid allocation with len valid elements already exhibits UB. That is, for any valid Rust program, we are guaranteed here that these two fields are "ok". So the only thing we need to make sure of is that the index "i" is inbounds, and that's trivial to do with an assert that panics if this is not the case. That is, at runtime, no program for which the index is not inbounds will reach the ptr.add(i) method, so there is no way to offset this pointer out of bounds, much less dereference it. Basically, because all safe Rust code can rely on all other safe Rust code upholding the rules, most of the proofs are really easy. The fact that you can prove safe abstractions over unsafe code in isolation from other abstractions is one of the main features of Rust. --- For synchronization primitives, proving the absence of data-races is particularly hard, and requires a lot of expertise. The subset of Rust programmers that actually need to do this is very small. Most people just use those primitives that have already been proven today, of which there are many.

nuerow 5y ago
> Using unsafe is like providing a "proof" that the code you write won't cause safe Rust code to exhibit undefined behavior. My take is that Rust is proposed based on the value proposition of its Safe Rust feature, but in the Linux kernel that feature has limited use. Therefore, if Safe Rust is out of the table then what's the point of writing/rewriting parts of the Linux kernel in Rust? What's the value proposition?
- volta83 5y ago
  > My take is that Rust is proposed based on the value proposition of its Safe Rust feature, but in the Linux kernel that feature has limited use. Where does your take come from? Everyone I've heard of proposing Rust for the Linux kernel does so almost exclusively by making the argument that Rust can create safe performant abstractions over unsafe code. That is, instead of requiring all Linux kernels programmers to be deeply familiar with RCU, you can have a small group of RCU experts create a safe abstraction over RCU, that then all other Linux kernel programmers can just use, without having to understand very deeply how it works. If they make a mistake, their code won't compile, and the error message explains why and how to fix it. This is a huge productivity boost for large complex projects, and a huge safety boost since these abstractions prevent a large set of security vulnerabilities, and these are the main reason I've seen people to use to introduce Rust into the Linux kernel. The fact that Rust does this with minimal - often zero - runtime overhead is a requirement for the kernel. But even for abstractions for which this is not the case, it still allows people to only have to become an expert when they want to improve performance, and any use of unsafe immediately triggers a requirement for such code to be reviewed by the actual experts. This is also a huge boon for these experts, since it substantially reduces the code they have to review. E.g. now they only have to review uses of the "unsafe RCU" APIs, instead of also having to review the uses of the safe RCU APIs, which is the case today. And also a big boon typically for the project in general, since it is much easier to attract "newbies" if there is stuff they can break. A newbie hacking on the linux kernel 20 years ago had much much much less to learn to become proficient than a newbie today. Reducing what newbies have to learn is a surprisingly effective way to increasing the contributor base of a project.
  - nuerow 5y ago
    > Where does your take come from? From this very discussion, for starters. > Everyone I've heard of proposing Rust for the Linux kernel does so almost exclusively by making the argument that Rust can create safe performant abstractions over unsafe code. The whole point is that the same thing (creating safe abstractions over unsafe code) is what developers have been doing with C for close to half a century. Therefore, there must be a value proposition regarding the use of Rust other than Safe Rust. I haven't heard one so far. In fact, I've read the exact opposite, such as compilers needing rewrites to accommodate that usecase. Thus, with Safe Rust out of the table, what exactly is Rust's value proposition? > This is a huge productivity boost for large complex projects, and a huge safety boost since these abstractions prevent a large set of security vulnerabilities, and these are the main reason I've seen people to use to introduce Rust into the Linux kernel. I feel those baseless assertions require some supporting evidence. Is there actually any tangible and concrete evidence that Rust, specially Unsafe Rust, improves productivity and safety? I'd love to read about it.
gpderetta 5y ago
>Using unsafe is like providing a "proof" that the code you write won't cause safe Rust code to exhibit undefined behavior It is more like providing an "axiom" as the compiler won't be able to check it and instead has to assume that it true. I wonder if there is scope to extend the language in the future to actually add machine checked proofs. Normally full machine checking doesn't scale to large projects, but if one had to restrict to writing proofs only for the small subset of unsafe code and let the simpler type/lifetime system handle the rest of the code it might be manageable.
- volta83 5y ago
  > It is more like providing an "axiom" as the compiler won't be able to check it and instead has to assume that it true. I don't think one should see this as an axiom, although as you mention one could. If your unsafe code allows safe Rust to exhibit undefined behavior, Rust makes no guarantees whatsoever about what your program will do. The convention in the standard library is to provide an actual proof that this won't happen as a comment to each unsafe block. Right now, there is no tooling to check these proofs, but there is a lot of ongoing research about how to do that, and the standard library already has some tooling to check things about this. > Normally full machine checking doesn't scale to large projects, but if one had to restrict to writing proofs only for the small subset of unsafe code and let the simpler type/lifetime system handle the rest of the code it might be manageable. That's the idea. It is not as simple as just proving each unsafe block independently, but rather all unsafe blocks within a Rust module must be proven together. From this point-of-view, it would make sense to only implement one unsafe abstraction per module, and keep these modules as small as possible, providing most of the implementation of the abstraction outside the module using only the safe API. Turns out, this is already how Rust code is written, since this is not only useful for writing proofs (either via assistants or using pencil and paper), but also helps humans reason about the correctness of the unsafe code by keeping all the "fluff" away.

nuerow 5y ago

> Using unsafe is like providing a "proof" that the code you write won't cause safe Rust code to exhibit undefined behavior. My take is that Rust is proposed based on the value proposition of its Safe Rust feature, but in the Linux kernel that feature has limited use. Therefore, if Safe Rust is out of the table then what's the point of writing/rewriting parts of the Linux kernel in Rust? What's the value proposition?

volta83 5y ago
> My take is that Rust is proposed based on the value proposition of its Safe Rust feature, but in the Linux kernel that feature has limited use. Where does your take come from? Everyone I've heard of proposing Rust for the Linux kernel does so almost exclusively by making the argument that Rust can create safe performant abstractions over unsafe code. That is, instead of requiring all Linux kernels programmers to be deeply familiar with RCU, you can have a small group of RCU experts create a safe abstraction over RCU, that then all other Linux kernel programmers can just use, without having to understand very deeply how it works. If they make a mistake, their code won't compile, and the error message explains why and how to fix it. This is a huge productivity boost for large complex projects, and a huge safety boost since these abstractions prevent a large set of security vulnerabilities, and these are the main reason I've seen people to use to introduce Rust into the Linux kernel. The fact that Rust does this with minimal - often zero - runtime overhead is a requirement for the kernel. But even for abstractions for which this is not the case, it still allows people to only have to become an expert when they want to improve performance, and any use of unsafe immediately triggers a requirement for such code to be reviewed by the actual experts. This is also a huge boon for these experts, since it substantially reduces the code they have to review. E.g. now they only have to review uses of the "unsafe RCU" APIs, instead of also having to review the uses of the safe RCU APIs, which is the case today. And also a big boon typically for the project in general, since it is much easier to attract "newbies" if there is stuff they can break. A newbie hacking on the linux kernel 20 years ago had much much much less to learn to become proficient than a newbie today. Reducing what newbies have to learn is a surprisingly effective way to increasing the contributor base of a project.
- nuerow 5y ago
  > Where does your take come from? From this very discussion, for starters. > Everyone I've heard of proposing Rust for the Linux kernel does so almost exclusively by making the argument that Rust can create safe performant abstractions over unsafe code. The whole point is that the same thing (creating safe abstractions over unsafe code) is what developers have been doing with C for close to half a century. Therefore, there must be a value proposition regarding the use of Rust other than Safe Rust. I haven't heard one so far. In fact, I've read the exact opposite, such as compilers needing rewrites to accommodate that usecase. Thus, with Safe Rust out of the table, what exactly is Rust's value proposition? > This is a huge productivity boost for large complex projects, and a huge safety boost since these abstractions prevent a large set of security vulnerabilities, and these are the main reason I've seen people to use to introduce Rust into the Linux kernel. I feel those baseless assertions require some supporting evidence. Is there actually any tangible and concrete evidence that Rust, specially Unsafe Rust, improves productivity and safety? I'd love to read about it.

gpderetta 5y ago

>Using unsafe is like providing a "proof" that the code you write won't cause safe Rust code to exhibit undefined behavior It is more like providing an "axiom" as the compiler won't be able to check it and instead has to assume that it true. I wonder if there is scope to extend the language in the future to actually add machine checked proofs. Normally full machine checking doesn't scale to large projects, but if one had to restrict to writing proofs only for the small subset of unsafe code and let the simpler type/lifetime system handle the rest of the code it might be manageable.

volta83 5y ago
> It is more like providing an "axiom" as the compiler won't be able to check it and instead has to assume that it true. I don't think one should see this as an axiom, although as you mention one could. If your unsafe code allows safe Rust to exhibit undefined behavior, Rust makes no guarantees whatsoever about what your program will do. The convention in the standard library is to provide an actual proof that this won't happen as a comment to each unsafe block. Right now, there is no tooling to check these proofs, but there is a lot of ongoing research about how to do that, and the standard library already has some tooling to check things about this. > Normally full machine checking doesn't scale to large projects, but if one had to restrict to writing proofs only for the small subset of unsafe code and let the simpler type/lifetime system handle the rest of the code it might be manageable. That's the idea. It is not as simple as just proving each unsafe block independently, but rather all unsafe blocks within a Rust module must be proven together. From this point-of-view, it would make sense to only implement one unsafe abstraction per module, and keep these modules as small as possible, providing most of the implementation of the abstraction outside the module using only the safe API. Turns out, this is already how Rust code is written, since this is not only useful for writing proofs (either via assistants or using pencil and paper), but also helps humans reason about the correctness of the unsafe code by keeping all the "fluff" away.