Re:My first verified imperative program
by sureglymop on Tuesday July 08, 2025 @12:40AM
(#44497130)
How so? If you specify the type int how would that save you from an overflow/underflow at runtime?
Re:My first verified imperative program
by alternatex on Tuesday July 08, 2025 @10:42AM
(#44500452)
Not sure if types are supposed to protect against overflow/underflow, it's more in the arithmetic territory. Interesting idea though, I wonder if some programming language allows overflow/underflow checks directly in the types.
Yes, it's actually quite easy:
+: (int<N>, int<N>) -> int<N+1> // or (int<N>, bit) as the return type
*: (int<N>, int<N>) -> int<2*N>
etc. Those are the actual types of those arithmetic operations.
If I can specify the type of my input I can ensure the verification.