> My understanding is that mypy and friends are not different. All those linters produce not only way to much false positives, no, they also produce false negat

> My understanding is that mypy and friends are not different. All those linters produce not only way to much false positives, no, they also produce false negatives (meaning that they let unsound programs pass; something that can not happen with a formally verified type system). I'm pretty sure the mypy and typescript devs would disagree here. The typescript and mypy abstract machines aren't any less sound than Java or c++. All four are abstract machines that make fundamentally similar guarantees. Cpp and Java can still encounter classcast exceptions and segfaults. And, like, you still need tests in functional languages. Specifically, I don't think I've encountered anything like > My code produced runtime errors which where actually "impossible"! The TS "type-checker" said things are such and such but at runtime they were different Without either explicitly subverting the type system, or dealing with some kind of untyped deserialization along an api boundary, which you absolutely need to test in any language.