> That's exactly right, and was my thesis; rust's type system does not allow you to prove the correctness of such a function, because it is neither correct nor incorrect without context. 'Unsafe', as a subversion of the type system which allows unsound behavior, is completely uninteresting wrt the topic at hand;

For the record, the “topic at hand” was the memory model not the type-system, nor the theorem proving capabilities of the borrow checker.

Your arguments are not wrong per se, but they are completely missing the topic.