Earlier quoted context omitted.
Ada has this without general dependent types AFAIK
Yes and no. The definitions are in the type system, but the checks are done at runtime, just like you would do manually. You don't really get the benefit of typing. The reason I can say that: you don't have to provide proofs that a value has to be positive to get things to compile.
There's some interesting work on making such contracts work well in a lazy language with higher-order functions.