> Right, because that's the only way to do it? What's wrong with that? Maybe the fact that it's wrong? Compile-time bounds checking is such a classic "hello wo

> Right, because that's the only way to do it? What's wrong with that? Maybe the fact that it's wrong? Compile-time bounds checking is such a classic "hello world" example for type checkers that it's become a cliche (eg. https://www.quora.com/What-are-some-good-examples-of-practical-applications-of-dependent-types-BESIDES-vectors https://www.quora.com/What-are-some-good-examples-of-practic... ) Dependent types make zero-overhead bound checking trivial. More recently, less powerful type systems like liquid types have been proposed (because reasons). Zero-overhead bound checking is usually on their feature list, since a) it's ubiquitous b) it's easy.