3 ms·

I've been programming with Standard ML pretty much since 1995, so I know a thing or two about powerful type systems. Of course there are different kinds of soft

I've been programming with Standard ML pretty much since 1995, so I know a thing or two about powerful type systems. Of course there are different kinds of software and different kinds of styles to write this software. Some software needs a correctness proof, other software doesn't, because if it seems to work, that is good enough. If your type system aligns well with the kind of correctness you need for your software, sure, that's good, go for it. A type system is better than nothing at all (that's why I much prefer TypeScript over JavaScript), but it is only an approximation of what you really want (your program fulfils its purpose). If that approximation is good enough for you and your problem domain, fine. Just be aware that the time you spend thinking about how to best fit of what you want to do into your type system, is probably not the best way to work on what to build and how to build it, although it might feel to you that way.

IshKebab 3y ago
> if it seems to work, that is good enough I think that's where many people would disagree with you. Also static types are not only about correctness. They also greatly help with understanding, documentation and navigation. The two biggest third party codebases I've contributed to are VSCode and Gitlab. VSCode was about 10x easier than Gitlab simply because I spent so much time in Gitlab just trying to find the code that a function called, or the code that called a function. (I think Ruby also encourages ungreppable code styles which makes this even worse.) In VSCode it was pretty much just one click. (Occasionally more because of abstract interfaces, but even then way way nicer.) Anyway yeah obviously if you don't really care about your code working or being readable then you are going to feel like static types are a waste of your time. That's kind of like saying that showering is a waste of time because you don't need to be clean.
- auggierose 3y ago
  > I think that's where many people would disagree with you. And they would be wrong, because for some classes of software, if it seems to work, that is actually the definition of working and fulfilling its purpose. Because there is no clear definition of what "correct" would mean. But that's not the point. Read my comments to see where I am coming from.
  - IshKebab 3y ago
    I guess you are talking about art projects? Yeah I don't think you can base a generic argument on a tiny niche programming domain.
    - auggierose 3y ago
      "some" is an existential quantifier. To prove an existential statement, you only need a single example. So of course I can base an argument on that, especially if it just illustrates the range of different purposes of software.
      - IshKebab 3y ago
        This is a debate, not a mathematical proof.
MaxBarraclough 3y ago
> the time you spend thinking about how to best fit of what you want to do into your type system, is probably not the best way to work on what to build and how to build it I think this is mistaken, but is getting close to the heart of the matter. The following describe identical sets: • Developers who know how to make effective use of a decent static type system • Developers who are able to follow a development methodology that deeply incorporates a language's static type system, such that the static type system becomes a useful tool integral to the development process rather than a hindrance Developers who view static type systems as just a nuisance - a malicious demon that must be propitiated at wasted expense - very often just lack the skills to make effective use of the type system. They mistakenly assume that it must not be possible at all, and that the folks speaking to the benefits of static type systems must just be talking nonsense. Many developers start out seeing static type systems as a hindrance, but gradually learn more about static typing and eventually come around to its advantages. I'm one such. I'm sure many of the really hardcore static typing folks (the wizards of Haskell and Scala) had the same experience. Anecdotally, it seems to me that relatively few developers tell the story in reverse, starting out with a deep competence in programming with static type systems and gradually coming around to dynamic typing. It sounds like you may have had exactly this experience, but I think this is uncommon. (Again, this is of course just anecdotal.) A similar thing goes for other software development skills such as version control. Plenty of developers start out seeing version control as frustratingly finicky and complex, but gradually build up mastery of their version control system and end up treating it as an integral part of their development process. Approximately nobody does this in reverse, abandoning a system like git for a free-form approach. All that said, there are times when heavyweight tools like static type systems and version control just aren't necessary. The applicability of their benefits and drawbacks do of course depend on context. > Some software needs a correctness proof, other software doesn't, because if it seems to work, that is good enough. I don't think this is meaningful. There is no seems to work, a bug either exists or it doesn't. > A type system is better than nothing at all (that's why I much prefer TypeScript over JavaScript) Pedantic nitpick: this implies JavaScript is an untyped language, which is not the case, it's a dynamically typed language. There are very few languages that lack a type system of any kind, pretty much just assembly and Forth. > it is only an approximation of what you really want (your program fulfils its purpose) Right, but no one is suggesting a type system can entirely replace a test suite. Static type systems offer only a fraction of the assurances of full correctness proofs, but are incomparably easier to use.

IshKebab 3y ago

> if it seems to work, that is good enough I think that's where many people would disagree with you. Also static types are not only about correctness. They also greatly help with understanding, documentation and navigation. The two biggest third party codebases I've contributed to are VSCode and Gitlab. VSCode was about 10x easier than Gitlab simply because I spent so much time in Gitlab just trying to find the code that a function called, or the code that called a function. (I think Ruby also encourages ungreppable code styles which makes this even worse.) In VSCode it was pretty much just one click. (Occasionally more because of abstract interfaces, but even then way way nicer.) Anyway yeah obviously if you don't really care about your code working or being readable then you are going to feel like static types are a waste of your time. That's kind of like saying that showering is a waste of time because you don't need to be clean.

auggierose 3y ago
> I think that's where many people would disagree with you. And they would be wrong, because for some classes of software, if it seems to work, that is actually the definition of working and fulfilling its purpose. Because there is no clear definition of what "correct" would mean. But that's not the point. Read my comments to see where I am coming from.
- IshKebab 3y ago
  I guess you are talking about art projects? Yeah I don't think you can base a generic argument on a tiny niche programming domain.
  - auggierose 3y ago
    "some" is an existential quantifier. To prove an existential statement, you only need a single example. So of course I can base an argument on that, especially if it just illustrates the range of different purposes of software.
    - IshKebab 3y ago
      This is a debate, not a mathematical proof.

MaxBarraclough 3y ago

> the time you spend thinking about how to best fit of what you want to do into your type system, is probably not the best way to work on what to build and how to build it I think this is mistaken, but is getting close to the heart of the matter. The following describe identical sets: • Developers who know how to make effective use of a decent static type system • Developers who are able to follow a development methodology that deeply incorporates a language's static type system, such that the static type system becomes a useful tool integral to the development process rather than a hindrance Developers who view static type systems as just a nuisance - a malicious demon that must be propitiated at wasted expense - very often just lack the skills to make effective use of the type system. They mistakenly assume that it must not be possible at all, and that the folks speaking to the benefits of static type systems must just be talking nonsense. Many developers start out seeing static type systems as a hindrance, but gradually learn more about static typing and eventually come around to its advantages. I'm one such. I'm sure many of the really hardcore static typing folks (the wizards of Haskell and Scala) had the same experience. Anecdotally, it seems to me that relatively few developers tell the story in reverse, starting out with a deep competence in programming with static type systems and gradually coming around to dynamic typing. It sounds like you may have had exactly this experience, but I think this is uncommon. (Again, this is of course just anecdotal.) A similar thing goes for other software development skills such as version control. Plenty of developers start out seeing version control as frustratingly finicky and complex, but gradually build up mastery of their version control system and end up treating it as an integral part of their development process. Approximately nobody does this in reverse, abandoning a system like git for a free-form approach. All that said, there are times when heavyweight tools like static type systems and version control just aren't necessary. The applicability of their benefits and drawbacks do of course depend on context. > Some software needs a correctness proof, other software doesn't, because if it seems to work, that is good enough. I don't think this is meaningful. There is no seems to work, a bug either exists or it doesn't. > A type system is better than nothing at all (that's why I much prefer TypeScript over JavaScript) Pedantic nitpick: this implies JavaScript is an untyped language, which is not the case, it's a dynamically typed language. There are very few languages that lack a type system of any kind, pretty much just assembly and Forth. > it is only an approximation of what you really want (your program fulfils its purpose) Right, but no one is suggesting a type system can entirely replace a test suite. Static type systems offer only a fraction of the assurances of full correctness proofs, but are incomparably easier to use.