Yeah, I don't disagree. It is a hard thing to do - you tend to get into messes with
dependently typed languages and so forth - one could easily argue that they're not quite ready
for writing kernels in!
Typically, you first implement maths in the type system, then you can implement a basic "is
smaller than" so then you could effectively arbitrarily refine the int range to be "the value
must be an int and must also be smaller than x". That kinda thing. Of course, as soon as you
hit "the value must be a function which will terminate", you're in trouble...!