<< Dependent type theories that are total and have a computable normalization procedure areTuring-incomplete. This is a theorem, not an opinion. Now, what the implications are for practical usability of dependent type theories that are total, that is an entirely different matter. >> [1] (slightly adapted: see the entire discussion for background)

Conversely, I would argue that Turing Machines are *not* an adequate model of
*computation*: there just is no such thing as a *machine* that does not
halt or crash or get switched off, *eventually*. And, *eventually* rather
goes with *interactively*.

In fact, more generally, the name of that "misunderstanding" is yet again *the
problem of infinity in standard mathematics and mathematical logic*.

[1] SE, Proof Assistants, "Possible root cause(s) of the misunderstanding that
DTT implies not Turing complete?"

https://proofassistants.stackexchange.com/q/4002/3006#comment7782_4002