3 ms·

> 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 – in

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

harimau777 3y ago
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.
- harimau777 3y ago
  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.
freilanzer 3y ago
> But is it wrong? Yes, because people don't "not often ship code in statically typed languages". It's obviously wrong.
- Spivak 3y ago
  I think you're taking offense on behalf of Java when the paragraph is dragging Haskel and Rust.
- randomdata 3y ago
  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?
  - freilanzer 3y ago
    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.

harimau777 3y ago

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.

harimau777 3y ago
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.

freilanzer 3y ago

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

Spivak 3y ago
I think you're taking offense on behalf of Java when the paragraph is dragging Haskel and Rust.
randomdata 3y ago
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?
- freilanzer 3y ago
  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.