In Ada? No dependent types, you just declare how to handle overflow, like declaring int16 vs int32 or similar. Dependent types means something entirely different and they are checked at compile time. SPARK uses something more like Hoare logic. Regular Ada uses runtime checks.
Whatever you want to call them, my point is that most languages, including Rust, don’t have a way to define new integer types that are constrained by user-provided bounds.
Dependent types, as far as I’m aware, aren’t defined in terms of “compile time” versus “run time”; they’re just types that depend on a value. It seems to me that constraining an integer type to a specific range of values is a clear example of that, but I’m not a type theory expert.
In Ada? No dependent types, you just declare how to handle overflow, like declaring int16 vs int32 or similar. Dependent types means something entirely different and they are checked at compile time. SPARK uses something more like Hoare logic. Regular Ada uses runtime checks.
Whatever you want to call them, my point is that most languages, including Rust, don’t have a way to define new integer types that are constrained by user-provided bounds.
Dependent types, as far as I’m aware, aren’t defined in terms of “compile time” versus “run time”; they’re just types that depend on a value. It seems to me that constraining an integer type to a specific range of values is a clear example of that, but I’m not a type theory expert.