Unsafe pure Rust code reflects a lack of expressive power. How raw memory becomes a typed object is a touchy area for arrays. To do collections safely, you have to be able to talk about an array which is partially valid. This is quite possible, but you need formal verification like constructs to do it. You need to be able to express that a slice of an array is valid, even though the whole array isn't.

If you can talk about a slice being valid, and an element being valid, you're almost there. It's a theorem that if an element is adjacent to the end of a slice, the element has some property, and all elements in the slice have a property, then a slice containing the original slice and the element has that property. Using that, you can prove by induction that as you grow a collection, the elements in use remain valid. If the access primitives don't let you access outside the valid range, they're safe.

With some extra predicates and a modest theorem prover, much unsafe code in the collection area could probably be proven safe.

Rather than describing unsafe code as a "dark art", it would be more useful to try to formalize safety in this way. The theory is well understood, and there are many proof of correctness systems around for other languages. It might require a lot of annotation in unsafe code, to help the prover along, but that's not a bad thing.