The problem with array out of bounds is that you'd need to reason about arithmetic expressions over natural numbers. However, in general that's a very thorny pr

The problem with array out of bounds is that you'd need to reason about arithmetic expressions over natural numbers. However, in general that's a very thorny problem since one runs squarely into [Gödel's incompleteness theorems](https://en.wikipedia.org/wiki/G%C3%B6del%27s_incompleteness_theorems https://en.wikipedia.org/wiki/G%C3%B6del%27s_incompleteness_...). Working around it requires painful restrictions or cause uncertainty over whether the compiler will apply certain optimizations.