Hacker News new | ask | show | jobs
by catnaroek 3611 days ago
> The only tests you have to discard (...) are some of the tests validating your input data.

That's not true. You can safely discard anything that tests something you've proven. A good type system doesn't only prove things for you - it also makes it easier to manually prove what the type system can't prove.
1 comments
shados 3610 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).

link
catnaroek 3610 days ago
> Something like TypeScript though? Only checks that variable types match.

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?

link