Funny it's not more common in high-level languages. You have types for non-negative whole numbers, whole numbers, larger whole numbers, not-whole numbers but imprecise, precise non-whole numbers but you usually can't tell compiler that one is in meters and one is in kilos and it shouldn't allow you to add one to the other.

Frink is one of the coolest things I've seen in languages development.