5 ms·

I have a beef with the typing section: > grug very like type systems make programming easier. for grug, type systems most value when grug hit dot on keyboard a

by mordae 3y ago

I have a beef with the typing section: > grug very like type systems make programming easier. for grug, type systems most value when grug hit dot on keyboard and list of things grug can do pop up magic. this 90% of value of type system or more to grug Juniors at my job routinely ship code that breaks due to null access in production, Sentry tells me. During intensive development periods that's about 1 detected null-access bug per day per junior developer. Using a proper type system with static checks would probably help immensely by pointing out "Hey, this can be null. You sure?" in their IDEs... Also, you can have completion even without static typing. > big brain type system shaman often say type correctness main point type system, but grug note some big brain type system shaman not often ship code. grug suppose code never shipped is correct, in some sense, but not really what grug mean when say correct That's just rude and uncalled for. I have shipped code mainly in in C, PHP, Python, Haskell and typed Python. The incidence of bugs that make it into production is much lower with typed languages. That's one reason to like it. It also makes refactoring much, much easier. I can check whole code base for broken callers when I change something widely used and get reliable results in seconds. That helps immensely with iterating on a growing code base.

dryanau 3y ago
I'm confused. The original article is in favour of typed languages. Aren't you in agreement?
- n4r9 3y ago
  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.
  - randomdata 3y ago
    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.
    - n4r9 3y ago
      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.
      - randomdata 3y ago
        > 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.
        n4r9 3y ago
        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.
randomdata 3y ago
> 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?
ragnese 3y ago
> 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.
xavierlint 3y ago
> 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.
nameless912 3y ago
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.

by mordae 3y ago

dryanau 3y ago

I'm confused. The original article is in favour of typed languages. Aren't you in agreement?

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

randomdata 3y ago

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

ragnese 3y ago

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

xavierlint 3y ago

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

nameless912 3y ago

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.