It's possible to do this (WUFFS does it) but it's so invasive that, well, you basically end up with WUFFS. You end up having to track every set of possible and impossible values at every location, etc. (during each program location too.) WUFFS certainly has its place and I've kind of been itching to try it out myself, but I think getting to the point where dynamic arrays can be statically bounds-checked would have highly disabled Rust.