Infinite precision intermediate arithmetic: how much would break?
The intermediate representation has to be infinite-precision for something like this to work correctly. (And it is much easier to implement with ints than with floats.)
I do think this is generally the correct approach to take, because it's both easy to use as a programmer and means you reliably get an error when overflow isn't handled correctly. However, there are a lot of cases that make it hard for a compiler to reason about. For example:
fn count_odd_elements(slice: &[usize]) -> usize {
let mut count = 0;
for element in slice { count += element % 2; }
count
}
Here, count cannot overflow because the length of the slice (and thus the number of loop iterations) is less than usize::MAX. But proving the lack of overflow requires reasoning about the code as a whole – the count += element % 2; line could potentially overflow if count were initialized to a higher value.
This makes me think that it would be very hard to retrofit an approach like this onto Rust: you would probably need to bake the reasoning about integer ranges into the entire language.
Discussion in the ATmosphere