> but that implies you need to statically prove that each index i for V[i] is less than N. So your code would be littered with such guards for dynamic indexing.

You just need a subrange type for i. Even PASCAL had those. And if you have full dependent types you can statically prove that your array accesses are sound without required bounds checking. (You can of course use optional bounds checking as one of many methods of proof.)