> A cooler feature would be requiring the compiler to prove the addition wouldn’t overflow.

Wuffs is specialized enough to do exactly that (https://github.com/google/wuffs).