Hacker News Reader

> That's just rude and uncalled for.

But is it wrong? Based on your stated experience, not even you seem to buy into type systems that force formal proofs – instead accepting lesser type systems that make tradeoffs between catching some problems (along with, most importantly, providing popup magic!) and not bogging you down in every little detail needed to prove total correctness.

> But is it wrong?

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

I think you're taking offense on behalf of Java when the paragraph is dragging Haskel and Rust.

Is it? When was the last time you saw, say, Coq in the wild? If you ever saw it you can be certain the program is correct, but I certainly have never seen it. Most likely because anyone using it really is still trying to satisfy the type checker.

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 for most circumstances, but maybe a primitive static type system somewhere in 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 good enough?

There is a difference between Coq and say Haskell, for example. I guess I will disprove your entire point by finding an unknown dynamic language that nobody uses then.

I think that it might be misguided. Excessively prioritizing how quickly you ship code is probably the single quickest way to summon the complexity demon.

Or maybe naïve would be more accurate? I could see how strict typing might not be needed if the developers write simple code on their own. However, in practice strict typing is necessary to protect yourself from developers who are unwilling to put in the effort to write simple code.

> That's just rude and uncalled for.

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'm confused. The original article is in favour of typed languages. Aren't you in agreement?

I think they differ about the why. The article claims that types are useful mainly because they allow sophisticated auto-completions. u/mordae thinks there are more important benefits re avoiding bugs in production.

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.

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.

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

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.

> That's just rude and uncalled for

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.

I've worked with a "big brain type system shaman" before. If anything, this is a very kind and charitable analysis. People who are obsessed with type hierarchies are _insufferable_ to work with, and their justifications often live in the land of "well what if"'s and "but that's not _sound_"'s. A lot of the enshittification that's induced by type systems comes from folks who believe that simply with enough types they will be able to completely prevent bugs, and that's just not true.