[randomdata]

> It's not about "truly valuing" one thing above all else

There is context here. With respect to the link, it is. It specifically refers to the "shamans" who promote that there is only one true type system way, and any "lesser" type systems are not sufficient.

C, typed Python, hell basically every language you are actually going to encounter in the typical programming project makes the very tradeoffs you mention because its probably not that important for the type system to perfectly express the constraints in order to validate correctness for your problems. That a primitive type system with some automated testing is good enough in the vast majority of cases. The idea, if you hadn't already figured it out before getting that far into the document, is to not overcomplicate things.

[n4r9]

The linked article says:

> big brain type system shaman often say type correctness main point type system

This is a much weaker position than you're suggesting. Opining about the "main point" of type systems does not mean thinking that there is one true type system way.