> 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.
Can 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.
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.