3 ms·

> You are basically trying to write a correctness proof before you actually have a good idea of what it is you are trying to build. I've done this plenty of tim

> You are basically trying to write a correctness proof before you actually have a good idea of what it is you are trying to build. I've done this plenty of times myself This is where I think the commenter towards the top of this thread has it right: > If your style is to hack hack hack until it’s right, yeah, types are challenging. If your style is to think first about types, you can also create guardrails in your code that naturally create the correct thing. Your experience with static typing is that of someone whose personal style is to write code as an exploratory process while you're trying to figure out what to build, and from the sound of it you were trying to do that in something like Java before you switched to TypeScript. And I completely agree—that style is a terrible match for a Java-like type system. But there are type systems besides TypeScript that are much more flexible than the kind that you're thinking of, and there are styles of software engineering that don't involve extensive prototyping as part of the development process. Those styles—typically slower and data-centric—combine really well with strong and flexible type systems (even something like modern Java with sealed interface goes a long way), and you're doing yourself a disservice by assuming that everyone who uses those styles is just wasting a lot of time.

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

auggierose 3y ago

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