This is true for some scenarios, like invalidating iterators through deletion (detected at compile-time by the borrow checker), but other scenarios still require runtime checks, right? Consider e.g. array out of bound accesses -- are you aware of approaches that move bounds checks to compile-time? It seems to me that this would be a painstaking process that would require programmers to annotate their code in many places to enable compile-time verification.