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

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.