2. Type systems have always been super limited in the kinds of bugs they can eliminate, even with "soundness".
3. This sounds like a type theorists point that is completely detached from most programming experiences.
Anyway JS's popularity is orthogonal to questions about efficient compilation. Types drastically simplify those, for you can work out at compile time how much memory needs to be allocated for each sub-expression of the program under execution. If you don't have types, you can only do that at run-time, and need extremely complicated JIT compiler technology to make this moderately performant.
(2) Sure. Still extremely helpful, all the more so, the bigger the software. If you don't have types to do this, you will have to find those bugs by testing -- much more labour intensive.
(3) Detached, maybe, but still true. To paraphrase Sutton's law: I'm detached from the toils of contemporary bread/butter programmers and look at verification because that's where the interesting open problems are.
- Enabling ahead-of-time compilation resulting in efficient code.
- Guarantees on the absence of specific classes of bugs. (This requires soundness.)
- Aiding verification. Types provide a rough classification of program behaviour which drastically simplifies verification. If you don't have types, your program logic needs to make typing information explicit in assertions.