Soundness is a constraint more than a feature. Having it limits what is possible in the language, forcing you into a smaller set of available solutions. So for

Soundness is a constraint more than a feature. Having it limits what is possible in the language, forcing you into a smaller set of available solutions. So for me it's not about running into unsound types regularly but how much complexity is possible and needs to be carved away to get at a working idea because of it. In TS I spend relatively a lot of time thinking about and tweaking minute mechanics of the types as I code. Where by comparison in ocaml (or more relevantly rescript) I just declare some straightforward type constructors up front and everything else is inferred as I go. When I get the logic complete I can go back and formalize the signatures. Because of the unsoundness (I think? I'm not a type systems expert) TS's inference isn't as good, and you lose this practical distinction between type and logic. And more subtly and subjectively, you lose the temporal distinction. Nothing comes first: you have to work it all out at once, solving the type problems as you construct the logic, holding both models as you work through the details.