A rhetorical question to keep in mind: would anyone take you seriously if you said ZFC is "not Turing complete" and therefore insufficient to express the algorithms that we write in mainstream programming languages?
First, what is the usual argument about total languages? The reasoning is as follows:
- In a total language, the function type $A → B$ classifies only1 the functions that are somehow able to be verified total.
- Any feasible verifier is going to reject some actual total definitions.
- Therefore, $A → B$ does not contain all Turing-computable, total functions from $A$ to $B$.
This reasoning is correct. However, what is not correct is the further assumption that to write a program accepts an $A$ and produces a $B$, it must be recognized by the system as a (total) function $A → B$. Certainly the total part is not the case in mainstream programming languages, because there $A → B$ means some class of partial functions from $A$ to $B$.
So, are total languages incapable of representing partial functions? No. There are potentially many ways to do it. One of the fancier ways is to define the free ω-complete partial order $A_⊥$ over a type $A$. Then the total functions $A → B_⊥$ act much like the partial functions from $A$ to $B$ from current (eagerly evaluated) programming languages.
From a practical perspective, this $A_⊥$ is not really very different from the previous coinductive definitions of a 'partiality monad.' The actual differences I can think of are:
The quotient inductive-inductive type (QIIT) would be a lot slower in certain scenarios, because it is based around representing successive approximations as $ℕ → A_⊥$ (note the similarity to emulating a partial recursive function using "fuel"). With the coinductive type, if you observe a value and get $\mathsf{later}\ x$, then $x$ is a value that represents something closer to the answer. The analogue of this with the QIIT is trying $f\ 0$ and getting $⊥$, so you need to try $f\ 1$, but there is no work shared between $f\ 0$ and $f\ 1$, it just restarts from the beginning.
The quotienting ensures that people can't quibble about the type "not really" representing partial functions, but something else. I think this might be the reason that people reject the coinductive version. You can observe how long its taking, and stop running at some point, so it's "not really" modelling partial functions, and therefore "not really" Turing complete. This is the reason why it has its advantages in #1, though.
So, even total languages without the features needed to faithfully represent the more 'topological' aspects of partial recursive functions have at least one way of representing practical aspects of them. If your 'main program' is allowed to be a total function of type $A → B_⊥$, with the proviso that it will (somehow) just be executed similarly to a partial function in a normal programming language, then there essentially aren't any $A$-to-$B$ programs that we genuinely can't express in this total language.
What does our argument above actually show in this light? That there are partial functions, i.e. total functions $f_⊥ : A → B_⊥$ that 'actually' converge to a well-defined value on every input, but we cannot exhibit corresponding total functions $f : A → B$, and prove that $f_⊥\ x$ converges to $f\ x$. But, this is also true of, say, ZFC (hence the earlier rhetorical question), the mathematical system often considered to underlie all our mathematical reasoning, including about programming. Some of the details differ a bit,2 but the discrepancy still exists.
And what is the limitation of not being able to recognize some actually total functions as such? It is good to be able to show that large parts of our program are (more) genuine total functions. But, if that is impossible or infeasible, we are not worse off by only recognizing them as an encoding of partial functions, so long as we are still allowed to execute partial functions as programs. As McBride says, we are actually more honest in distinguishing recognizably total functions from partial functions, which most languages don't do. Another major use for total function is that they make sense to use in dependently typed languages for calculations that happen (and must terminate) during type checking, and we can't just use partial functions for those purposes. But most 'Turing complete' languages also don't let you do this. Many don't have anything like this period, and at best you usually get a stilted total language to program in at the type level, rather than one that has comparable convenience to the value level.
There are engineering questions to be considered. For instance, neither the QIIT nor the codata solution seem like the ideal encoding from a performance perspective. It's possible (something like) the QIIT is actually not as bad as I made it seem, if the runtime executor can somehow pass it a fake value that makes a 'limit' actually run with infinite "fuel," and never have to restart from scratch. That'd take care, though, and probably still have overhead. These are questions about efficiency of the representation of partial functions, though, not whether or not they can be represented.
1: For the purposes of this answer, where a programmer would care what functions they are able to write syntactically and get accepted by the language. The fact that there are mathematical models of the total language where the semantics of $A → B$ includes things that are not the image of any syntax doesn't help them write the missing programs as total functions.
2: E.G. you might be able to define non-computable ZFC functions that 'actually' correspond to converging partial recursive functions, but not prove that the partial recursive function converges to the values of the non-computable function. Whereas in a total programming languages, the functions are all expected to be computable, so you'd be stopped at the step of defining the corresponding function, rather than the proof that the function is computable.