if you cannot implement the algorithm in a Turing machine, you cannot implement the algorithm in any system. This isn’t formally proven, but it’s empirically held up for a long-ass time. Nothing can be more powerful than a Turing machine.

whereas the Wikipedia pages states:

Since, as an informal notion, the concept of effective calculability does not have a formal definition, the thesis, although it has near-universal acceptance, cannot be formally proven.

So the article makes it sound as if it’s an open question – “it might be proven, but hasn’t been yet” – while Wikipedia makes it sound like it’s nonsense even to speak of proving it, because you can’t prove an informal claim.

I’m immediately reminded of TECO, which had a Turing-complete keystroke language. Of course, TECO didn’t have anything similar to Vimscript, so TECO extensions were written in the keystroke language, the most famous of those extensions being the original version of Emacs.

A very nice proof, and delightfully short as well. Honestly I’m not the least bit surprised by this ;)

I’m missing a reference to a resource which proves that m-tag systems (for m >= 2) are Turing complete, could you add that? Thanks!

Added a bunch! The history of the proof turns out to be a bit more complicated than I thought.

That error macro cancelling trick was very cute.

I enjoyed that.

One question: The article states:

whereas the Wikipedia pages states:

So the article makes it sound as if it’s an open question – “it might be proven, but hasn’t been yet” – while Wikipedia makes it sound like it’s nonsense even to speak of proving it, because you can’t prove an informal claim.

Which is correct?

The wikipedia page

I’m immediately reminded of TECO, which had a Turing-complete keystroke language. Of course, TECO didn’t have anything similar to Vimscript, so TECO extensions were written in the keystroke language, the most famous of those extensions being the original version of Emacs.