3 ms·
I'm working on a research language with an extra set "explicit math operators" which expose carry in, carry out, etc. explicitly, and doesn't do type promotions
by rab_oof 12y ago
I'm working on a research language with an extra set "explicit math operators" which expose carry in, carry out, etc. explicitly, and doesn't do type promotions and signals errors on under/ overflow.
"+!" If you want C-like behavior.
It'll be imperative with full dependent types as well.
Also interesting: cryptol, Irdis, coq, but the work is on making generic systems programming clear as possible in a static, imperative language without a titanic runtime or crawling along with superfluous assertions.
- nullc 12y agoCarry bugs in limbed bignum code don't usually result in integer overflow (though integer overflow does usually mean the code is busted for sure). Part of the reason for this is that it's common to use 'overcomplete' representations where the limbs are smaller than the underlying type so that multiple operations can be performed before propagating the carries all at once. This class of error is very much behind all the noise making I did at the Rust development team about treating integer overflow as a first class cause of software disaster as much as they have memory safety. Fortunately, they seem to be moving off the everything-wraps and wrapping-is-always-fine position.