The type system is not sound… that is there are things which the type checker cannot prove.
Not that the languages themselves are unsound.
Not that the languages themselves are unsound.
2. What I meant to ask was: what does satvikpendem mean by "JS is unsound"? It's a dynamically typed language, so they can't be talking about soundness in the type system...
> The central result we wish to have for a given type-system is called soundness. It says this. Suppose we are given an expression (or program) e. We type-check it and conclude that its type is t. When we run e, let us say we obtain the value v. Then v will also have type t. - https://papl.cs.brown.edu/2014/safety-soundness.html
This only makes sense in the context of static types afaict, because you do not "typecheck an expression" in a dynamically typed language.