> putting limits on the scripting language

Putting limits on a scripting language should not be too hard (even without talking about any correctness proof). And I would bet that for a scripting language where the limits are in a way that "in a correct implementation, it should be highly likely that these limits are actually enforced" (i.e. the specification of the scripting language has no parts that makes you suspicious whether there exists some loophole that a malicious actor could use to overstep the limits), it should actually be possible to write a verified implementation with some effort.

But this is not what people want: for example, basically every evolution of the web standards since HTML5 by the WHATWG was about extending what is possible to do in the scripting language (JavaScript).