I'm pretty sure Ada's ranged integer is tested dynamically, not statically. It's still a cool language feature. To get a static detection of integer overflow,

I'm pretty sure Ada's ranged integer is tested dynamically, not statically. It's still a cool language feature. To get a static detection of integer overflow, I think that you need to use some variation of dependent typing. So it's possible in Liquid Haskell. And of course, it's easily done in dependent-typed languages like Agda, Coq, and Idris. Edit: I had earlier written Nim has this static range checking capability, but it looks like it also uses a runtime check.