Explicitly ranged integers as seen in Ada are also very nice, there’s no reason that traps should only occur at the 32-bit or 64-bit boundaries.
Pascal had that. Somehow it got lost.
The formal verification community ignored integer overflow for far too long
Well, we didn't, back in the early 1980s.[1] But I had that argument with other people in the formal verification community.
I once wrote a paper called "Type Integer Considered Harmful". (Unfortunately, I've lost this.) This was back in the era when there were mixed 16-bit and 32-bit integers as machines transitioned to 32 bit. My position was that it was the compiler's job to size intermediate expressions so that overflow couldn't occur there if it wasn't going to occur in the final result. Overflow in the final result should be detected at run time or proved impossible.
Here's what that means. Consider
uint_32 a,b,c;
a = b + c;
Overflow of "b + c" implies overflow in a, so we just have to check for overflow.
uint_32 a,b,c,d;
a = b + c - d; // ordered as (b + c) - d
Overflow of "b + c" does not imply overflow in a. So the "b + c" sum has to be done in 64 bit.
uint_32 a,b,c;
a = b * c;
Again, overflow in "b + c" implies overflow in a, so we don't need a bigger intermediate value.
uint_32 a,b,c,d;
a = (b * c) / d;
The "b * c" term needs to be 64-bit.
uint_32 a,b,c,d,e;
a = (b * c * d) / e;
Either we need 128 bit arithmetic, or refuse to compile this. Some expressions you just can't do right with the machine hardware. The user could write
uint_32 a,b,c,d,e;
a = (uint_32(b * c) * d) / e;
which means trapping on overflow if "b * c" is bigger than an uint_32, and
the compiler must generate a 64-bit product for "uint_32(b * c) * d)".
Languages tend to view numeric type conversion as a named type problem, rather than a numeric range problem. That leads to wrong answers in some cases. The goal is to get the right answer or trap.
If you want unsigned arithmetic that wraps, you would write
uint_32 a,b;
a = (a + b) % (2^32);
The compiler should recognize this as an optimization and do 32-bit unsigned wrapped arithmetic without trapping. The programmer says what they mean, rather than relying on the semantics of the hardware, which might change. (This used to be a bigger issue when we had to support 36 bit and 48 bit CPUs. There are still some odd-size DSP chips.)
Pascal had that. Somehow it got lost.
The formal verification community ignored integer overflow for far too long
Well, we didn't, back in the early 1980s.[1] But I had that argument with other people in the formal verification community.
I once wrote a paper called "Type Integer Considered Harmful". (Unfortunately, I've lost this.) This was back in the era when there were mixed 16-bit and 32-bit integers as machines transitioned to 32 bit. My position was that it was the compiler's job to size intermediate expressions so that overflow couldn't occur there if it wasn't going to occur in the final result. Overflow in the final result should be detected at run time or proved impossible.
Here's what that means. Consider
Overflow of "b + c" implies overflow in a, so we just have to check for overflow. Overflow of "b + c" does not imply overflow in a. So the "b + c" sum has to be done in 64 bit. Again, overflow in "b + c" implies overflow in a, so we don't need a bigger intermediate value. The "b * c" term needs to be 64-bit. Either we need 128 bit arithmetic, or refuse to compile this. Some expressions you just can't do right with the machine hardware. The user could write which means trapping on overflow if "b * c" is bigger than an uint_32, and the compiler must generate a 64-bit product for "uint_32(b * c) * d)".Languages tend to view numeric type conversion as a named type problem, rather than a numeric range problem. That leads to wrong answers in some cases. The goal is to get the right answer or trap.
If you want unsigned arithmetic that wraps, you would write
The compiler should recognize this as an optimization and do 32-bit unsigned wrapped arithmetic without trapping. The programmer says what they mean, rather than relying on the semantics of the hardware, which might change. (This used to be a bigger issue when we had to support 36 bit and 48 bit CPUs. There are still some odd-size DSP chips.)[1] http://www.animats.com/papers/verifier/verifiermanual.pdf