[feanaro]

Yet languages with totality checkers and coinduction like Idris exist. These allow you to make useful but provably terminating programs. Humans are able to construct these termination proofs, though presumably not for all programs.

In practice, this means that the reductive take of Turing completeness, the halting problem and Rice's theorem is misleading in some way.

Yes, there is no general algorithm for constructing termination proofs for any arbitrary Turing machine. But there are clearly classes of problems for which a biological computer (a human) is able to construct termination proofs and proofs regarding other semantic properties.