@julesh - "Basic question but I'm not 100% sure: it's not possible to have a "reasonable" syntax that captures exactly the total computable functions N → N, right?"
I'm pretty sure that's true, but we should phrase it in theorems so we can spot loopholes. Here's what I know. The set of total computable functions is not computably enumerable: there's no total computable function f: ℕ²→ℕ such that every total computable function ℕ→ℕ is one of the f(i, -): ℕ→ℕ. The proof is an easy diagonal argument.
So then the question is whether "a reasonable syntax that captures exactly the total computable functions ℕ→ℕ" must give a way to computably enumerate these functions.