Simpler mental model for unsafe

This is unfortunately extremely untenable. Taken to the extreme, you're arguing that I can't rely on functions like i32::wrapping_add or ptr::wrapping_offset to be correct. All proofs have and should state their assumptions, and a flood-fill view of all potentially soundness relevant code could be useful (or uselessly highlight everything), but asking unsafe code to only rely on unsafely delivered guarantees needlessly restricts unsafe code from using safe abstractions and expands the domain of when you're expected to use unsafe from "downstream safe API misuse could potentially use this to cause UB" to "downstream unsafe could potentially use this to avoid causing UB."

By relying on upstream safe APIs for your own soundness, you're essentially opting in to considering their relevant correctness issues as your soundness issues. Perhaps think of it like an unsafe fn i_checked_it which attaches a proof to an otherwise safe implementation.

Or, alternatively, there's an implicitly attached proof burden to the unsafe that you don't call the downstream code in a way that causes soundness relevant correctness issues.

Regarding Rust unsafe as an untyped proof assistant, then yes, capturing every single bit of proof logic beyond "the AM primitives are correct" into an unsafe carrier has utility. But the superpower of Rust is zero fanfare "FFI" between safe Rust and unsafe Rust; insisting that safe functionality is rewritten into "proof assistant Rust" before it's usable from unsafe Rust goes against that ideal that all code should be safe if possible.

Unsafe Rust shouldn't rely on complicated invariants of safe code, only simple correctness properties that are unlikely to regress. But this is just good engineering practice, anyway — reduce the soundness relevant complexity surface to make reasoning easier. And utilizing safe API assists in such encapsulation of invariants.

3 Likes