3 ms·

No, I don't neglect that. These guardrails are guiding you towards something, but it is very optimistic to assume that they guide you towards the best solution.

No, I don't neglect that. These guardrails are guiding you towards something, but it is very optimistic to assume that they guide you towards the best solution. There is a lot of religion and faith involved here. I care a lot for logical consistency and soundness, probably more than anyone else you know. But it is wrong to think that static type systems are the best way towards this. Logic is the best way towards this, and static type systems are just one way of implementing logic, and not the best one. Especially in programming, what static type systems were really good at, was automating some correctness checks. I believe in a future where automation gets so good that static type systems become a hindrance, and where their benefit vanishes when weighed up against your freedom to express things as they really are.

naasking 3y ago
> These guardrails are guiding you towards something, but it is very optimistic to assume that they guide you towards the best solution. "Best solution" is a fantasy. Any solution must be expressed in a language with concrete semantics, but there is no best language for all possible problems. This was the lesson of Kolmogorov complexity. Therefore, we will always necessarily be using a suboptimal language, and we should let go of any wish for ill-defined optimality. We should instead use a language that guides towards engineering good solutions to problems with desirable properties. Sometimes that might mean strict control over resources (as with Rust), sometimes that isn't necessary (so OCaml,F#, etc. would do). An empirical fact of engineering is that most mistakes people make are trivial, eg. typos, one off errors, forgetfulness to change code in all relevant places during refactoring, etc. Good abstractions enforced by static types solve all of these problems, allowing you to focus on the core problem without being bothered that you might have missed some silly details. Yes the compiler bothers you to correct these details, but this is typically simple mechanistic work that nevertheless can't be automated by any other language without sacrificing other desirable properties. I'm not going to argue that any static type system is better than no static types, because it's easy to invent a bad type system. We've had pretty damn good type systems since the 70s though, they just didn't see much use until recently.
- auggierose 3y ago
  "Best solution" is a proxy here for the software you really want. That's what you need to go for; if you don't, I don't really want to use your software, although I might have to, because there is nothing else. Again, a good general type system that catches simple mistakes is better than nothing, I agree with you here! But Rust for example, isn't that. It is quite invasive in terms of how you have to think about your program, and if your way of thinking or your particular problem aligns with Rust's approach, great. Most of the time, it will not. So if you choose for example Tauri over Electron, most of the time, that will be the wrong choice. Anyway, static type systems are a crutch. They've been useful in the past, mainly because they allow to automate partial correctness. In the future, we will have something better (I am not saying we will have something "optimal", although it might feel that way compared to the current state of things).
  - naasking 3y ago
    Yes, Rust is invasive because it guarantees certain properties that are otherwise very difficult to guarantee, and by all reports, once you build the requisite mental model it becomes much more straightforward, which is typical of static typing and programming in general. Re: static typing being a crutch, I disagree, and I think more, better typing is in our future, not less. We'll see how it goes.
    - auggierose 3y ago
      But let's be clear what we are talking about here, so we can see who wins the bet: I am betting against static typing, but on general logic. So I am betting against a static type system being the future, instead I think a general logic will be the future, not only of programming, but of all engineering.

naasking 3y ago

> These guardrails are guiding you towards something, but it is very optimistic to assume that they guide you towards the best solution. "Best solution" is a fantasy. Any solution must be expressed in a language with concrete semantics, but there is no best language for all possible problems. This was the lesson of Kolmogorov complexity. Therefore, we will always necessarily be using a suboptimal language, and we should let go of any wish for ill-defined optimality. We should instead use a language that guides towards engineering good solutions to problems with desirable properties. Sometimes that might mean strict control over resources (as with Rust), sometimes that isn't necessary (so OCaml,F#, etc. would do). An empirical fact of engineering is that most mistakes people make are trivial, eg. typos, one off errors, forgetfulness to change code in all relevant places during refactoring, etc. Good abstractions enforced by static types solve all of these problems, allowing you to focus on the core problem without being bothered that you might have missed some silly details. Yes the compiler bothers you to correct these details, but this is typically simple mechanistic work that nevertheless can't be automated by any other language without sacrificing other desirable properties. I'm not going to argue that any static type system is better than no static types, because it's easy to invent a bad type system. We've had pretty damn good type systems since the 70s though, they just didn't see much use until recently.

auggierose 3y ago
"Best solution" is a proxy here for the software you really want. That's what you need to go for; if you don't, I don't really want to use your software, although I might have to, because there is nothing else. Again, a good general type system that catches simple mistakes is better than nothing, I agree with you here! But Rust for example, isn't that. It is quite invasive in terms of how you have to think about your program, and if your way of thinking or your particular problem aligns with Rust's approach, great. Most of the time, it will not. So if you choose for example Tauri over Electron, most of the time, that will be the wrong choice. Anyway, static type systems are a crutch. They've been useful in the past, mainly because they allow to automate partial correctness. In the future, we will have something better (I am not saying we will have something "optimal", although it might feel that way compared to the current state of things).
- naasking 3y ago
  Yes, Rust is invasive because it guarantees certain properties that are otherwise very difficult to guarantee, and by all reports, once you build the requisite mental model it becomes much more straightforward, which is typical of static typing and programming in general. Re: static typing being a crutch, I disagree, and I think more, better typing is in our future, not less. We'll see how it goes.
  - auggierose 3y ago
    But let's be clear what we are talking about here, so we can see who wins the bet: I am betting against static typing, but on general logic. So I am betting against a static type system being the future, instead I think a general logic will be the future, not only of programming, but of all engineering.