|
|
|
|
|
by bjz_
3143 days ago
|
|
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. |
|