For those interested, the proof for the Turing-complete and nearly-TC (as in total functional programming) cases is the same as the proof of the time hierarchy theorems[1], and for finite-state-machines the proof is based on results showing that verification of a (concise program expressing) finite state machine is PSPACE-complete. Those results are not surprising, as it is easy to see how any problem in computer science can be reduced (efficiently) to verification, so being able to efficiently prove correctness of a language capable of describing algorithms with super-polynomial complexity (this, BTW, only requires the ability to loop/recurse to depth 2) would mean contradiction.

[1]: https://en.wikipedia.org/wiki/Time_hierarchy_theorem