[Tracking Issue] What we can and cannot say about Unsafe Rust

[felix91gr]

The gist of why this issue exists is this:

The memory model for Rust is not yet complete. This means that what is considered UB in Unsafe Rust has not yet been 100% specified.

In this issue, I will try to keep an up-to-date list of:

1. For which things in Unsafe Rust there is consensus of Undefined Behavior.
2. What Open Questions remain about Unsafe Rust.

Both items will be most certainly incomplete. Help is appreciated!

---

I will also keep a list of:

1. Important Discussions in this topic (blog posts, Zulip threads, etc)
2. Ongoing Research aimed towards a complete memory model for Rust
3. Sources of documentation about Unsafe Rust
4. Tools for directly dealing with or diagnosing Unsafe Rust
   (note: this is probably something where the Tooling Subcommittee has the jurisdiction)

[rcseacord]

How can you use a language for safety-related software that doesn't have a defined memory model?

[felix91gr]

How can you use a language for safety-related software that doesn't have a defined memory model?

1. Install it
2. Create a project with it
3. Write it
4. And then deploy it

That's about it, really

[felix91gr]

Well in reality it's more nuanced than that, right? There aren't many languages with the low-level capabilities of Rust. And in fact, there are none with its alias analysis (apart from Cyclone), which is a big part of why Rust works.

Anyway, what I'm trying to say is that there's a lot of innovation here, and that innovation takes time. The language turned 10 just this year! And the foundational math framework needed for borrow checking (separation logic) is only 26 years old.

The opsem team is trying to find a memory model that:

1. Reflects what is considered "sound practice", in a formal way.
2. Does not restrict optimizations that could be considered reasonable to do for a "sound" program.

All of that gets defined carefully, in a mathematically precise way. Examples of sound and unsound code get analyzed, and memory model candidates are tested against them (with things like Miri).

One could "just" adopt a memory model from another language, but since Rust innovates so much in how we reason about memory, none will be an exact fit. Many things have been taken from the experience of other languages, like for example the ordering of atomic operations, which I believe was largely copied from C++. But not all of them.

There are many things that have been proven about Rust. I'll try to dig up the links (I will have to for this post, because they are part of the Ongoing Research section), but for example the Safe subset of the language has basically been proven to be absent of UB. And that already gives you a guarantee that about 90%+ of your code is safe by default. Furthermore, great effort has been put into proving exactly what needs to be done behind a Safe API for Unsafe code, so that one can guarantee that said API is also always free of UB.

This in practice means that one can build foundations with unsafe, carefully attest their properties, and then build safe APIs on top of them that will never have UB.

That's how one can:

use a language for safety-related software that doesn't have a defined memory model.

Does that make sense? @rcseacord I hope that makes sense