formalizing a statement about the expressive power of programming languages wrt divergence In the Coq'Art book the authors mention in passing that any language that can calculate all computable functions must also be able to express diverging computations.
Or in other words, there can be no Coq' that is Turing-complete that maintains the guarantee that all computations describable in that language terminate.

How would I go about formalizing this statement? I feel it's a simple corollary to the Halting problem, but I don't know enough about formal semantics of programming languages to express or prove this.
Let us take a somewhat simplified view of a programming language as a mapping $C$ (the compiler) from finite strings of characters (source code) to descriptions of Turing machines (machine code). A description of a Turing machine is just a finite string of characters of a certain kind. And since finite strings of characters are computably isomorphic to natural numbers (we can computably encode string as numbers and vice versa), we can pretend that both source code and Turing machines are described by numbers.

Under this view a programming language $C$ is a partial map from natural numbers to natural numbers which accepts a number $n$ (the source code) and either diverges or returns a number $C(n)$ (the "compiled" Turing machine). It makes sense to require that $C$ is a computable map, i.e., that there is in fact a Turing machine that calculates it, otherwise magic is required to understand the programming language.

Note that I can enumerate all possible outputs of $C$. I simply try $C$ on every input in parallel by dovetailing, and whenever any parallel copy gives a result, I enumerate it. Let $f : \mathbb{N} \to \mathbb{N}$ be an enumeration of all outputs of $C$.

Let $\phi_k$ be the partial computable map that is computed by the Turing machine described by the number $k$.

We now come to the crux of the matter. Suppose $f$ enumerated precisely the total computable maps, i.e., $\phi_{f(n)}$ is a total computable map for all $n \in \mathbb{N}$, and for every computable map $g$ there is $n$ such that $g = \phi_{f(n)}$. Consider the computable map $d(n) = 1 + \phi_{f(n)}(n)$. This map is total because $\phi_{f(n)}$ is total for every $n$. There is $j$ such that $\phi_{f(j)} = d$, but then $\phi_{f(j)}(j) = d(j) = 1 + \phi_{f(j)}(j)$, contradiction.

The conclusion is that $f$ cannot possibly enumerate precisely the total computable maps. Therefore it either misses out some total maps, or enumerates some partial ones.