> 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 a

> 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.