> A type system can never catch all bugs True, but that doesn't mean we shouldn't try to improve the type system. We've already seen large improvements in the

> A type system can never catch all bugs True, but that doesn't mean we shouldn't try to improve the type system. We've already seen large improvements in the past in TypeScript and flow. For example, nullable types were not there in the beginning but were added to the type system because they are immensely useful. Making the type system sound would be another such improvement. If you start with that premise, why not "A type system can never catch all bugs, therefore let's not use it at all"? Sounds stupid, doesn't it? > The most important goal - if you value reliable programs - is that the code is intelligible to people. The code that's running the airplane I'm sitting in, I don't give a fuck whether it's intelligible. Though I do care very much that it has been formally proven to be correct. Having a sound type system is pretty much a prerequisite for formal proofs. Also, intelligible code and soundness are not exclusive. What makes you think that? I can write unreadable looking code in JavaScript and Haskell. And I can write beautiful, readable, concise code in both languages, too.