In aviation, there is the notion of "dual path", which means two ways to do anything. Each functions as a backup to the other.

The best dual path systems are when they use different technology. Hence, an error in one is highly unlikely to infect the other.

This is what static typing provides.

I guess people who are against static typing are not working on aviation type projects - more like worst thing that can happen on what they work is a div slightly off.

Dealing with bugs is the most time consuming part of programming. Static typing errors are most welcome because they are detected by the compiler and can be fixed promptly.

I like this analogy. Another one I have used is double-entry bookkeeping.

I'm definitely going to steal double-entry bookkeeping from you. Someone will invariably dismiss aviation safety analogies as histrionics, but everyone can get "you want your money correct, right?".

> Someone will invariably dismiss aviation safety analogies as histrionics

I encounter that regularly, as I often use aviation analogies to guide me in programming. D's design has been significantly influenced by my aerospace experiences.

Talk about missing the point, but sure, whatever works for you.

Bob Martin uses that already for tests. And I think it's a much better analogy for that.

That being said, I myself do prefer types over tests. I just don't know of a better analogy...

Ah, a great analogy. I wish I'd thought of that!

I wouldn't say it's disproportionate. Strong static typing is massively valuable for humans too. Maybe it's just more obvious to some people because you actually can write the same large program twice using the same "person" and a different language.

Previously studies into the benefits of static typing for humans were always a bit flawed because you can't do that with people. And tbh I don't know why but there are a surprising number of people that don't appreciate static typing. My guess is a combination of ego and laziness, which doesn't apply to LLMs.

> strong types are disproportionately valuable in LLM coding vs human coding because they essentially function as context and the typechecker actively enforces correctness

One could argue that this was a large benefit for human coding long before LLMs became useful.

It is why I always preferred strongly-typed languages.

And once we had practical strongly-typed languages with implicit type inference I really couldn't wrap my head around why anyone would prefer dynamic typing other than just inertia due to that being what they were used to.

It's basically a myriad of unit tests without writing them down (in full).