Higher-order primitive recursion

[ncfavier]

I got slightly confused by the following claims:

https://github.com/andrejbauer/notes-on-realizability/blob/8dccd94381ec3bb343aa68ceed74b47b880ace32/notes/models.tex#L2161

https://github.com/andrejbauer/notes-on-realizability/blob/8dccd94381ec3bb343aa68ceed74b47b880ace32/notes/models.tex#L2367-L2371

Together with https://github.com/andrejbauer/notes-on-realizability/blob/8dccd94381ec3bb343aa68ceed74b47b880ace32/notes/introduction.tex#L99-L101 they seem to imply that the Ackermann function is not definable in Gödel's system T, or in assemblies over an n-tpca; but it is, because those have higher-order primitive recursion (or primitive recursive functionals), which is more powerful than first-order primitive recursion (see here for some discussion around this). I think this ought to be clarified somewhere (maybe all three places?).

This leads me to ask: are nr-tpcas actually used anywhere in the notes? It seems like, for the purpose of interpreting logic or type theory, which are "total" languages, they are not that useful.