Ada provides integers and floats with range checks, and you can specify the underlying size, but intermediate values don't get checked. It also has a separate

Ada provides integers and floats with range checks, and you can specify the underlying size, but intermediate values don't get checked. It also has a separate form of unsigned integers called "modular types" which expressly indicate wrapping, if that's your intent. -- Range checked equivalent of uint64_t; type Nibble is range 0 .. 15 with Size => 64; -- Every assignment is as if Value := (Value % 16); type Wrapped_Nibble is mod 16; type Small_Float is digits 4 range 0.0 .. 20.0 with Size => 32; I agree that the subexpression issue is problematic, IIRC I thought this was checked in SPARK code, but I could be wrong. The big benefit is describing your intent and you know that the stored value is in range, though whether it went outside of that range in calculation might not be known. Another thing is that these types define 'First, 'Last, 'Pred, 'Succ, and 'Range attributes which you can use. for N of Nibble'Range loop -- do something end loop;