[kuruczgy]

> Your type system cannot be sound. It's going to have escape hatches and exceptions because that's how dynamic languages roll.

I think you could prove that you can't construct a sound & complete type system for Lua. But just saying "Your type system cannot be sound" by itself is definitely wrong. I don't understand why people are throwing out both soundness & completeness, instead of at least retaining one (and I think the choice here is pretty obvious, a sound but incomplete type system is much more useful than an unsound one).

From Flow's website[1] (a type checker for JavaScript):

> Flow tries to be as sound and complete as possible. But because JavaScript was not designed around a type system, Flow sometimes has to make a tradeoff. When this happens Flow tends to favor soundness over completeness, ensuring that code doesn't have any bugs.

I don't understand why other type systems for dynamically typed languages cannot strive for that, and in particular I am pretty salty at TypeScript for explicitly not caring about soundness.

[1]: https://flow.org/en/docs/lang/types-and-expressions/#toc-sou...

[lolinder]

Why, though? Completeness matters more than soundness in practice for this kind of language, which is a large part of what gave TypeScript its edge. The only people who complain about soundness seem to be those whose approach to TypeScript is one of theoretical interests rather than practical application.