See my comment to @Capricorn2481 here[0]. You seem to be saying that unsafe code can be made correct so as to ensure soundness. This can be done by verifying invariants in unsafe code, but it is generally discouraged, as it tempts large unsafe blocks that could be partially safe code. Both you and @Capricorn2481 don't seem to make the distinction between "arbitrary safe code" and "my safe code within the module with unsafe", which is a crucial part of the idea of writing encapsulated unsafe. Technically, I believe unsafe code can still be made sound in the presence of arbitrary safe code, but it would have to tiptoe around violating memory safety, lowering its utility and performance substantially, if not completely.