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.
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.
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'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?
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.
"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.
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).
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.
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.
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 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.
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.
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.
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.