**UPDATE**: I would probably talk about this different now that I know a bit more about how something like this would *actually* be formalized, but this post is an analogy more than an actual formal model, even if a variation can be formalized.

There is a fair amount of confusion about what `unsafe`

means in Rust, as well as debate about how one should think about it. Recently I’ve seen several blog posts like What is Rust’s unsafe?, The Temptation of Unsafe and Unsafe as a Human-Assisted Type System.

So I’ll ~~add yet more useless philosophizing~~ provide another perspective.

I’m not really attempting to explain what is considered unsafe in Rust, which is explained by the reference. Nor am I going to try to answer the question of precisely when unsafe should be used and how often.

My basic suggestion: we can think of `unsafe`

in terms of mathematical axioms and theorems. This understanding is somewhere in between actual mathematical rigour and an analogy.

### Terminology

**Unsafe block**

An unsafe block,`unsafe {}`

allows potentially unsound actions like dereferencing a raw pointer or calling an “unsafe function”. Code attempting these actions outside an unsafe block or function fails to compile. The code may (and should) be sound, but the compiler cannot verify this.**Unsafe function**

Declared with`unsafe fn`

, an unsafe function can perform all the actions that are possible in an`unsafe {}`

block, but is also unsafe to call.**Soundness**

“Unsound” code is any code triggering undefined behavior. Undefined behavior is a rather complicated concept that is important to understand especially for C programmers, but also C++ programs and anyone using the`unsafe`

keyword in Rust. This series of LLVM blog posts is helpful.Safe code should always be sound (barring compiler bugs and calls to incorrectly implemented functions containing unsafe blocks). Correct uses of

`unsafe`

are also sound. So “unsound” code is unsafe code that fails to correctly uphold the invariants safe code relies on.Other terms are used; often just “safe”. But it gets a bit consfusing to talk about things like “safe uses of unsafe”. And more importantly, it’s then ambigous to say how “doing $x is unsafe”, which could mean $x it requires

`unsafe`

and the programmer must maintainer certain invariants, or that $x always results in undefined behavior.

### Safe code

One important subgoal of programming in Rust is to proof your program is sound and free of undefined behavior. (You also want to verify that behavior is actually the behavior you want, performance is acceptable, etc.).

The glory of Rust is that you can “prove” this, as long as all your code from `main()`

down doesn’t use `unsafe`

.

```
fn main() {
let mut v = Vec::new();
.push(42);
v}
```

We can think of this as going along with a proof:

**Theorem:** `main()`

is sound

**Proof:**

- Assume
`Vec::new()`

and`Vec::push()`

are sound - If
`main()`

compiles, it follows from the compiler’s checks that`main()`

is sound

This proof is valid as long as we have corresponding proofs for `Vec::new()`

and `Vec::push()`

, and assume the compilers rules for verifying the soundness of safe code are correct. The proof is rather short since it’s core argument is simply rustc said so. We’ll consider the implications of this reasoning later.

By writing `fn main()`

without the `unsafe`

keyword, and not using an `unsafe {}`

block in the body, and assuming the code compiles, we have written a proof that the `main()`

function is sound. This applies equally to other functions we might write and call (directly or indirectly) from `main()`

.

### Functions with unsafe blocks

But… at some point you are almost certainly dependent on unsafe code. At least in the standard library.

Consider `Vec::push`

, for instance:

```
pub fn push(&mut self, value: T) {
// This will panic or abort if we would allocate > isize::MAX bytes
// or if the length increment would overflow for zero-sized types.
if self.len == self.buf.cap() {
self.reserve(1);
}
unsafe {
let end = self.as_mut_ptr().add(self.len);
ptr::write(end, value);
self.len += 1;
}
}
```

We use `unsafe {}`

when the compiler cannot prove the soundness of our code. So it becomes an axiom.

**Axiom:** `Vec::push()`

is sound

Thus our “proof” for the soundness of `main()`

relies on this axiom. This is only true if the `ptr::read`

call is correct; but the compiler isn’t able to verify this, and relies on the programmer to assert that it is.

### Unsafe functions

Now let’s instead consider an `unsafe fn`

; in particular, `Vec::set_len()`

:

```
pub unsafe fn set_len(&mut self, new_len: usize) {
debug_assert!(new_len <= self.capacity());
self.len = new_len;
}
```

This defines neither a theorem nor axiom. Generally, the fact that it’s an `unsafe fn`

suggests some uses are sound and others are not; without clarifying what uses or allowing the compiler to check this.

But the documentation does provide what could be considered an axiom:

Safety

`new_len`

must be less than or equal to`capacity()`

.- The elements at
`old_len..new_len`

must be initialized.

Or, restated:

**Axiom:** Suppose `new_len <= capacity()`

. Suppose elements at `old_len..new_len`

are initialized. Then it follows that `unsafe { v.set_len(new_len); }`

is sound.

Given this axiom, we can “prove” our use of `set_len`

is correct; but the compiler cannot verify these requirements.

### Ideal world: encoding and proving invariants in Rust

Ideally we’d be able to encode these requirements in Rust. Then our caller could provide some proof that the invariants are met, and call the function without using `unsafe {}`

. Similarly, our `set_len()`

and other `Vec`

methods could have soundness proofs, assuming the stated constraints are met.

Thus, use of `unsafe {}`

could be limited further to only cases that are correct but impossible to prove (under the provided system) or where it would be too difficult to prove.

I’m not the first one to think such a feature would be nice, but it would be rather complicated. So for now, we rely on the programmer verifying these properties themself. It’s probably not something the language will even have, but perhaps some external tool could provide some form of this for users who require it.

But without that, it’s still important to include this information in the documentation. A well-written library should provide an “axiom” of this sort in the documentation of any `unsafe fn`

(at least in the public API). Rust’s ability to encapsulate unsafely isn’t much use if it isn’t possible to determine what uses of the function are sound.

### Implicit axioms

Our programs are dependent on `unsafe`

code whether or not we realize it: at least in the standard library. As we see above with `Vec`

, the standard library contains `unsafe {}`

blocks, so our list of axioms include those defined by these usages.

Perhaps less obviously, the language itself also implicitly defines various axioms. The exact behavior doesn’t have a mathematical specification, but we could list some easily enough:

**Axiom:** It is sound to consecutively execute two sound blocks of code

**Axiom:** In safe code, the lifetime checker correctly prevents lifetime violations

**Axiom:** An if statement is sound if the condition, body, and else block are sound

And we could continue, until we have a fairly large but finite set of axioms.

A soundness bug in the standard library or compiler thus can make or program unsound. This is rare, but occasionally happens.

### Limitation: unsafety extends beyond function block

Our model is made a little less neat by a common subtly of unsafety, as mentioned in the Nomicon:

Because it relies on invariants of a struct field, this unsafe code does more than pollute a whole function: it pollutes a whole module. Generally, the only bullet-proof way to limit the scope of unsafe code is at the module boundary with privacy.

The example there is different, but applies to the implementation of `Vec`

as well. Which you might have been wondering about, if you noticed that the implementation for `set_len()`

above (unlike many uses of `unsafe fn`

) would still compile without the `unsafe`

keyword. All it does is set the `.len`

member, with fairly ordinary safe code.

But this could lead to problems in combination with other code. The `push()`

code above would be unsound if, for instance, another function had set `self.len`

to a bogus value. So even though setting `.len`

is safe, carelessly changing it could cause methods like `.push()`

to produce undefined behavior.

So my neat idea that a function can correspond one-to-one with a soundness theorem or axiom isn’t quite perfect, at least without more assumptions, since different methods of a type like `Vec`

interact in ways that could allow safe code in one to trigger undefined behavior in the unsafe code of another. But perhaps the idea is still somewhat useful.

### Limitation: not formally specified/verified

Rust does not have a formal specification, so there is no official list of axioms like this. For true mathematic rigor, we would also need a formally verified compiler proven to generate code conforming to these axioms. Computer-verified proofs can be done written and checked software like Coq, which provides an elaborate type system that can prove theorems using the Curry-Howard correspondence.

There have been efforts toward formal verification in Rust. But a full formal specification and formally verified compiler, especially one that is also performant, probably isn’t really feasible.

This doesn’t invalidate the general reasoning here, but we have to be careful not to be too bold to claim things are really “proven” in a rigorous mathematical sense.

### Conclusion

In an ideal world, a major aim of compilers is proof checking. The type checker proves that types are used correctly. The optimizer creates smaller, more efficient code and proves it’s behavior is equivalent. The lifetime checker in Rust proves the liveness of references.

In practice the mathematical rigor involved here is lower than in an ideal (and unrealistic) world. But we can still reason about these things in terms of the concept of mathematical proof.