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