Inductive number types seem pretty appealing here. A type like "Nat = Zero | Succ Nat" is 100% always correct by construction and can be safely transformed into

Inductive number types seem pretty appealing here. A type like "Nat = Zero | Succ Nat" is 100% always correct by construction and can be safely transformed into raw integers (and operations thereon) by the compiler. And it is also precisely the correct number type for array indices. If you can open your mind to dependent types, then Fin is even better, which also avoids overflow by construction. But then again dependent types are a whole different beast when it comes to compilers and language capabilities and so on.