[cfallin]

> The proof of this is that several core concepts that are considered "safe" have "unsafe" portions that make let work

I think this is actually a common pattern in many different domains. For example, the OS kernel's virtual memory subsystem does many things with "unsafe" primitives -- it has direct access to page tables and can map anything anywhere -- yet it provides a "safe" abstraction of isolated process address spaces.

The way I think about it is that you have to define basic building blocks somewhere. It's not reasonable to build a static analysis that understands the N different varieties of smart pointers, and refcounting, and dynamically-checked mutability (RefCell), and custom allocators (TypedArena), and all that. It's much more elegant to separate concerns, have only raw pointers and lifetimes/borrowing built-in, and put those pieces together in "blessed" ways with all the unsafe code in one place in the library. If you try to build that understanding into the compiler instead, you're just moving the same unsafe-has-to-be-correct algorithm down one level, and unnecessarily complicating things.