[randomdata]

In the link, Grug acknowledges the benefits of correctness established by types to an extent, but is highlighting the diminishing returns. After all, if one truly valued type system-enforced correctness, they would be writing code in something like Coq, not C and typed Python.

[n4r9]

That sounds like a false binary to me. All language features have trade-offs and interactions with other features. It's not about "truly valuing" one thing above all else - your relative preferences depend on your experiences and what you value in the product.

Some people think type correctness is very important; perhaps they value minimising bugs over shipping fast. Other people think auto-complete suggestions is more important; perhaps they value shipping fast over minimising bugs.

Both positions could well-justified depending on the domain. In healthcare or military, the former makes sense. In gaming or web development, the latter makes sense.

[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.