Liquid Types [1] achieve the same in existing programming languages: no bounds checks at runtime, and reject programs without an in-bounds proof.

For a demo, see "Scrap your Bounds Checks with Liquid Haskell", giving a 6x speed up in high-performance parsing of UDP packets.

[1]: https://news.ycombinator.com/item?id=37349276 "A Gentle Introduction to Liquid Types"

[2]: https://github.com/Gabriella439/slides/blob/main/liquidhaske... "Scrap your Bounds Checks with Liquid Haskell"