Refinement types and Dependent types can do all of that. But you are right that mainstream languages ca’t do that today. Hopefully that will change.