Any recent popular languages with similar support for types of Ada? Is such type system being costly to implement the reason not many other languages pick up the feature?
Haskell has `Numeric.Natural` but I don't think you can define an integer constrained to a range. It probably goes beyond what the type system can do (statically). I think it's possible with Dependent Types (in Idris) but this is rather new.
For example, if SPARK (Ada subset) is used and absense of runtime errors can be proved by GNATprove, then runtime check generation can be disabled in Ada compiler.
GNATprove generates verification conditions (conjectures) from SPARK code and assertations. Then it feeds these verification conditions to proof tool (Why3, Alt-Ergo, CVC4 or Z3).