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.

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.

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

But is it wrong? Based on your stated experience, not even you seem to accept type systems that force formal proofs – instead accepting lesser type systems that make decent tradeoffs between catching some problems (and providing popup magic!) without bogging you down in every little detail.

Yes, because people don't "not often ship code in statically typed languages". It's obviously wrong.

Clearly type systems live on a spectrum with varying degrees of sacrifices made, with each sacrifice compromising some ability to check for correctness, but giving back some other advantage, improved developer productivity being one possibility.

It is not a question of static typing or not – it is how complicated of a type system do you really need? Even Grug agrees that dynamic typing is not sufficiently complicated, but maybe a static type system that falls somewhere around the middle of the spectrum that helps catch the most grievous of errors (and provides popup magic!) with a sprinkling of automated testing to fill in the gaps where the type system falls short is best for the vast majority of programming situations?

It's just a joke. I'm almost certainly one of the people he's poking fun at and I don't think we should get bent out of shape. He obviously thinks that C or Java levels of static typing are fine/good, and thinks that fancier stuff like found in Rust and Scala is a waste of time. I think he's dead wrong, but that's life.

I think you're not the "shaman" he's referring to.

By "big brain type system shaman" I understood someone who doesn't necessarily write code, but instead, e.g. sells courses around the topic, getting people hyped about it, etc.

He uses the word "shaman" previously when talking about Agile, and there are many who fit that picture of working on selling courses, and not on developing software.