[luchak]

I think you're confusing the extent of what is possible in your current type systems with what is theoretically possible with types.

Why can't a type system keep track of units? Why can't it be aware of precision? If it's possible for you to find a proof that a particular implementation of your algorithm won't fall into an infinite loop, then there is a type system that can verify that your algorithm will terminate. Of course, actually designing a sound type system with this property could be quite tricky, and I have no idea what the resulting language would look like -- but it would be possible.