I'm not convinced that formal provability as a goal for a language generally used to write web front-ends makes a lot of sense. The "gaps" in TypeScript's type

I'm not convinced that formal provability as a goal for a language generally used to write web front-ends makes a lot of sense. The "gaps" in TypeScript's type system are actually escape hatches which allow clean-ish interoperability with the code that people in the real world actually use. Like, dammit, JQuery and all the other filthy things that make web pages go. That code is already written and no one is going to change it to make the TypeScript typings "work". Such code by the way is usually incompletely (or even incompetently!) typed but perfectly servicable in practice.