That would require a formal model of how 'unsafe' works, and we still don't have that. Pointer provenance is an especially difficult issue, also affecting C/C++ specification efforts.
Indeed, we don't have that model, and we definitely need it. I don't think it's intractable. We've made a lot of progress. I would like to see more focused effort on this particular problem from the academic community.