No, not if your language has totality checking like Idris, Agda, Lean, etc. Granted, it can sometimes be finicky to prove totality - the type checker naturally has to be a little conservative due to the impossibility of solving the halting problem, but for most things with array bounds checking it shouldn't be an issue.
integers with additions are decidable - that's pretty much what you need to verify array bounds (multiplication with a constant is included as well, so matrices should work too).
Do you mean "in practice" that's what you need? I could buy that, but I'm thinking about it in terms of the language spec. What would it say? Are we moving toward a language spec that says the meaning is "whatever the reference compiler can handle"? Or do you mean one that says "array indices may only be (constant) linear combinations of variables in order for the code to be compilable" or something like that?
Good point. The way I imagined is, the language is defined as "safe", and has both "static" and "dynamic" guarantees. Whatever the compiler is able to prove statically, amazing, or else it adds dynamic checks. The programmer can optionally tag the function/expression so that the compiler will warn if it can't prove it. Long-term, I think it's very reasonable to assume the solvers will improve, so best to design a language with this in mind.