In almost all (strongly typed) languages, there is still a need for runtime checks like divide by zero and array bounds checks. Certainly languages like Rust & Haskell bring a high level of static analysis and that is good when you are relying on the tool for memory safety.
Personally I prefer gradual type systems that need less up front wrestling so that the coding process is more productive, more time can be spent on tuning the design rather than “finally I made it work” acceptance of compiler driven design. Such languages such as Python, Raku use GC for safety so not perfect for embedded or OS type tasks but easier on the brain.
I mentioned Raku since it has extensive runtime type support which allows code like:
subset Zero of Int where * == 0;
subset NonZero of Int where * != 0;
multi infix:<div>(Int \a, Zero \b) {warn “you dolt”; Inf}
multi infix:<div>(Int \a, NonZero \b) {a div b}
So Larry Wall chose to leverage a runtime typesystem to make it easier to write and maintain code rather than go down the straitjacket route.
> Personally I prefer gradual type systems that need less up front wrestling so that the coding process is more productive, more time can be spent on tuning the design rather than “finally I made it work” acceptance of compiler driven design.
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.
Static vs Dynamic vs Gradual… it’s really more a question of “how does my brain like to get to a solution and keep it functioning” and I find that fascinating.
> it’s really more a question of “how does my brain like to get to a solution and keep it functioning” and I find that fascinating
Sure, but this is largely a matter of training and experience. Plenty of fans of dynamically typed languages just haven't learnt how to make effective use of decent static type systems.
Static type systems are premature optimization, and come with all of its problems.
So a more fluid solution is a great thing, if done right. TypeScript comes to mind, although it has other problems, in particular mutable data structures by default.
Why do you say that static type systems are a "premature optimization"? On its face, that seems like a (very spicy) opinion that's been stated as fact.
It is a fact, that is why I state it as one. 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, and it is a good way to waste time and tell yourself you are productive. Yes, I am also looking at all the "let's rewrite stuff in Rust" projects.
Especially problematic is that the type system doesn't necessarily reflect the correctness you care about, but just some properties the language cares especially about. You are spending your time trying to shoehorn your solution into somebody else's idea of correctness, who doesn't really know anything about your program at hand.
That's why I like TypeScript, its type system is expressive enough for many simple correctness checks I actually care about, while at the same time not getting (too much, and with the above caveats) in the way of how I think about what I build.
It is especially clear to me that static type systems are dinosaurs of the past. The future is on-the-fly checking of arbitrary logical properties of your program, which can always contain what static type systems used to be for as a subset.
> 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.
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.
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.
> 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.
"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.
> 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.
> Especially problematic is that the type system doesn't necessarily reflect the correctness you care about, but just some properties the language cares especially about.
You're neglecting that these guardrails guide you towards solutions that can be naturally expressed and checked by the language. That's a feature, not a bug.
> The future is on-the-fly checking of arbitrary logical properties of your program, which can always contain what static type systems used to be for as a subset.
Yeah, except for logical consistency or soundness, but who cares about that?
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.
> 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.
"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).
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.
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.
The misconception that all "early optimization" is premature optimization is a dangerous one.
I'll agree with you that starting with static type systems is an early optimization. But if it's premature or not is clearly context dependent. And it is often "right on time" optimization. Just as are many things engineers like to deride as "premature optimization".
It's not premature if it's known to be needed and the cost of doing it later greatly outweighs doing it now.
I've been getting a lot of mileage out of Julia recently, and would counter that plenty of fans of statically typed languages just haven't learned to use an effectively-typed dynamic language.
I like Raku (it fits my brain as I was programming a lot of Perl in the 90s) and I like these features. You want to be able to do this. A lot of this you can easily make static though (so you have both) (maybe that happens under the hood?).
Personally I prefer gradual type systems that need less up front wrestling so that the coding process is more productive, more time can be spent on tuning the design rather than “finally I made it work” acceptance of compiler driven design. Such languages such as Python, Raku use GC for safety so not perfect for embedded or OS type tasks but easier on the brain.
I mentioned Raku since it has extensive runtime type support which allows code like:
So Larry Wall chose to leverage a runtime typesystem to make it easier to write and maintain code rather than go down the straitjacket route.