[kingkilr]

Sure you can.

First, in a philosophical sense: pointers and x86 CPUs are real, ultimately any safe abstraction must be built on unsafe primitives. The ability and need to do that aren't specific to memory unsafety, we do that all over software engineering.

Second, empirically, my experience has been that the design of these abstractions can be safe, but moreover that the cordoning off of unsafe blocks makes 3p auditing for memory unsafety _much_ easier to do. It can be orders of magnitude faster than reviewing an entire C or C++ codebase.

[Kednicma]

A TCB should be dozens of lines, not thousands. More code means more places for more bugs to hide.

My experience in Safe Haskell was that, if you have to ask each module individually whether it has a safety property, then you've already created too much work for yourself. Instead, require every module to structurally encode the desired invariant.

Or, in fewer words: If you want memory safety, don't have `unsafe` blocks.