|
|
|
|
|
|
by shados
3611 days ago
|
|
|
A good type system, yes. Something like TypeScript though? Only checks that variable types match. We're a far cry from ML/Elm/Scala/Haskell here. So the only thing it helps is get rid of bad tests (eg: tests that check a function return any string...tests you shouldn't write even in a purely dynamic language). |
|
|
TypeScript's type system is unsound, so you can't rely on the type checker alone to prove anything useful. However, manually proving things about TypeScript programs is still easier than doing so with JavaScript programs.
I don't believe it's practical to rely on type checkers to prove absolutely everything. There are mathematically proven upper bounds on how much you can automate reasoning. For instance, global type inference only works with first-order type languages. Higher-order anything flies out of the window, yet higher-order properties of programs need to be proven!
What we ought to do is find the optimal division of labor between automated and manual proving, always keeping in mind that the optimal case isn't being able to prove something. The optimal case is not having to prove it because it's obviously true. How do we design a programming language so that more interesting things are obviously true?