Types as they exist today provide shapes. But they dont provide l external limits. Every single type safe language Ive used (limited) merged together these concepts in the form of a stdlib pattern mixed with a “choose your own adventure” library or pattern. For example in typescript we use TS and lean heavily on zod. You cant avoid it. In TS especially you just have structural types so you have to filter everywhere on user defined or external data structures. Never mind setting limits on sizes, iterations, etc.

I think the primary problem is that the second we cross network or system boundaries all the guarantees go out the window. You have to be very defensive at every layer. If we’re ever able to encapsulate that in a type system that would be… impressive.