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.