4 ms·
> Type systems to me seem to be (I'm not exaggerating) the answer to all software reliability problems (barring social ones). If you want a property to uphold,
by tome 9y ago
> Type systems to me seem to be (I'm not exaggerating) the answer to all software reliability problems (barring social ones). If you want a property to uphold, formulate it as a type. The compiler verifies.
I'm a massive Haskell proponent and I'm calling you out because you're doing typed programming a massive injustice with this kind of overinflated claim. There is no known type system that can get anywhere near solving "all software reliability problems". Flexible type systems like Haskell's are really useful. Don't overpromise.
- tpush 9y agoSo where does it fall down? Excluding the social ones I mentioned.
- tome 9y agoCan you prove the correctness of a sort function in the type system? I don't know any mainstream language where you can do that. You'd have to go to something like Agda, Idris, Coq or F* which are hardly practical languages (currently). Beyond that there's an entire universe of complexity that we have no idea how to prove (practically) in the type system. Haskell types encode simple properties. They're extremely useful properties in practice but they don't come anywhere near "everything" we would want to prove.
- open_bear 9y agoWhat do you think about clojure.spec approach?
- empthought 9y agoThose aren't proofs at all, and the docs even say so.