> 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.)
Yes, as I said, you must use bounds checking or dependent types or effects or monad returns.
Arrays are the effect choice in most languages. The signature as a function becomes a gnarly continuation passing if you insist on the equivalence and so most people just tend to think of it imperatively.
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.)