> You can't isolate unsafe operations from only having isolated effects to the block of code flagged.

You can focus your manual verification efforts on unsafe code. That is pragmatic. “Well, shit happens, and I can do nothing about it” is not.