As I'm reading the movfuscator paper by Stephen Dolan, I encounter this claim:
In order to have Turing-completeness, we must allow for nontermination.
This seems like a reasonable statement. But I'm also aware of this work by Wouter Swierstra which aims to prove quite the opposite (as I see it): that one can simulate a Turing-complete machine in a total language such as Agda.
From a purely theoretic point of view: I'm somewhat confused. Total languages permit only total functions, and total functions always terminate. Yet there exists a total interpreter of a Turing-complete language. Can somebody help reconcile this confusion?
Is nontermination necessary for Turing-completeness? Is this a valid question at all?