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, s

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 https://news.ycombinator.com/item?id=37349276 "A Gentle Introduction to Liquid Types" [2]: https://github.com/Gabriella439/slides/blob/main/liquidhaskell/slides.md https://github.com/Gabriella439/slides/blob/main/liquidhaske... "Scrap your Bounds Checks with Liquid Haskell"