I would love to have something that would translate a more human readable version that looks like a constraint or range that internally translates to the same functionality of the peano solution. If that's what you're saying Rust intends to have then I'm very excited and continue to be impressed by the progress there.

https://github.com/rust-lang/rfcs/blob/master/text/2000-cons... is the current accepted design; we plan to go further in the future, but wanted something minimal at first. This is likely to land in nightly by the end of the year and be stable sometime early next year.

Doesn't Ada have this ability where you define numeric types with a range?

Yes, like so

  type jump_by_tenth is delta 0.1 range 1.0 .. 99.0;

Yes but afaik it translates to runtime checks.

It cannot be done in compile-time in general case. Rice's theorem forbids. Every non-trivial property of a program (like whether result of this function lies in this range for all inputs in that range) is undecidable.

ETA: I'm not completely correct. Ada could have used something akin to 2-complement overflow handling, that is forcing every operation on a range to have a result in the same range, but it introduces runtime overhead too.