> I would assume that the vast majority of memory access can be statically proven safe if you throw enough money at the problem, meaning the bookkeeping can be eliminated.
You can't really do this without adding the same sorts of annotations as Rust or Safe C++. Especially if you care about keeping modular/separate compilation and code reuse.