> 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).

This article mentions a few of the reasons why some of our best attempts at defining languages that are "trivially correct" keep failing.

Among other examples, it specifically mentions that you if lego together two Push-Down Automata chatting with each other you get a Turing Machine back out. It doesn't include my other favorite recent example that we found a 0-day sandbox escape in the Universal Turing Machine itself.

The problems generally keep coming back to the Church-Turing Hypothesis that if you've got one Turing Complete language you've got theoretical access to them all.

Turing Completeness in turn seems an "emergent property" rather than a hard bar to clear. Rule 110 [0] shows Turing Completeness in the mathematical equivalent of a petri dish. We've built Turing Machines out of Magic the Gathering card game decks [1].

To some extent if there was a way to build a truly, well enforced, secure scripting language you would think that we would have already found it given how important it would be to security and to safety.

[0] https://en.wikipedia.org/wiki/Rule_110

[1] https://www.toothycat.net/~hologram/Turing/index.html