Thank you for the correction, I'll edit my comment.

sometimes the proof that the access is

safe is bevond what the compiler is able to represent

Could you say a few more words about this? In what situations do you have to write 'unsafe-tagged' code blocks? Could this be changed by improvements to the compiler? Or is it necessitated by the type of task being done by the code?