My experience is that there's a correlation between powerful type systems and the property that once your program compiles, it's correct. Compiles == correct is rarely true in C or JavaScript. It's often true in Haskell and Rust. TypeScript is somewhere in between C and Rust.

There's a niche available for a language which is relatively easy for a human to read, but with a very powerful at the expense of difficult to use type system. The language would let you make all sorts of assertions whose meaning are easy for the human to see, but to compile would need to come along with correctness proofs. The language is meant to be written by AI, which can battle the compiler, and write the proofs, but then read by humans who can verify that the AI wrote the program they wanted and/or direct the AI to make changes.