> At what point does the additional cognitive burden of advanced type system features become a worthwhile tradeoff for program correctness? It seems to me that this depends wholly on the complexity of the program.

I have similar thoughts as those expressed by the sibling post by danharaj (ohai Dan!), but I'd like to stress a particular point: the type system lowers the cognitive burden, rather than increase it.

By way of analogy, think of it this way: spoken languages are quite complex; you have all sorts of stuff to get right:

* conjugation

* noun genders

* tenses

* participles

* prepositions

* etc, etc, etc...

And there are all sorts of fun, intricate grammatical rules that govern which words are supposed to go where. That's a ton of work!

Now, one could argue: wouldn't it be much easier if we just, you know, made the language simpler?

The problem is that each of these things serves some purpose (well, mostly, anyway -- dunno how I feel about, say, gendered nouns); for example, if we stripped away the ability to convey tense, the language would become simpler, but it would lose out on some important expressive power.

While we're at it, we could also shorten the vocabulary. Picking an arbitrary number, let's say we keep only the top 100 words. That'll probably capture most of the essentials, if what is "essential" is "that which ensures you get your basic needs for survival".

But let's say "love" wasn't in that top 100: how would you tell someone that you love them?

That's no problem: whenever we want to tell someone we love them, we can unpack the definition:

love: a gentle feeling of fondness or liking

Uh-oh -- "gentle" and "fondness" didn't make the cut... I suppose we'll unpack those definitions as well. So now we have:

love: a (mild in temperament or behavior; kind or tender) feeling of (affection or liking for someone or something) or liking

Oh hell, temperament certainly isn't in the top 100, so here we go again:

love: a (mild in (a person's or animal's nature, especially as it permanently affects their behavior) or behavior; kind or tender) feeling of (affection or liking for someone or something) or liking

So ...

... yeah, that got out of hand pretty quickly, and we still have a ways to go.

The next time you tell someone you love them, think about how incredible it is that you have a word at your disposal that immediately conveys something so nuanced. Think of all the meaning that's cram-packed into that one word. And it's only one syllable!

So how does this exercise relate back to more advanced type systems?

A sophisticated type system (like Haskell's) allows me think (and express) thoughts that I otherwise wouldn't be able to. I mean, with inordinate amounts of effort (kind of like the effort I would need to keep the whole, fully unpacked definition of "love" in my head all at once), I might be able to do everything I was able to do before -- it would just make things more difficult, and it wouldn't be practical.

Programming in weaker languages (e.g. Java, Go) often feels like trying to tell someone something as seemingly simple as "I love you", but all I have at my disposal is the ability to grunt and flail my arms around -- that's a simpler system, but man is it a lot of work.