[nitroll]

It is, especially if these checks are done at compile time, not at runtime.

[berkut]

How can checks be done if the size is dynamic based on run-time data?

[prodigal_erik]

"Integer between 0 and n-1 inclusive" is the type of valid indices for an n element array. The trouble is most languages don't have type systems that allow expressing that.

[pjmlp]

The Pascal family are such languages.

[102910201]

Expect a blog post within four hours "Rust has solved the halting problem!"...

[prodigal_erik]

Even when you can't prove what arbitrary code does, proving what well-written code does is useful, and not writing unprovable code would be a small price to pay.