[mkleczek]

There are two problems with this:

1. Even for as weak computational model as FSM the problem of verifying its correctness is intractable (NP-hard). And modularisation does not help.

2. We don't know any weaker computational model that is strong enough to be viable for the problems we want to solve and still weaker than TM. It is well known that it is surprisingly easy for a language to be (accidentally) Turing complete.

[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.

[ncmncm]

It is not necessary to verify that random presented machines have some property. It suffices that we can reliably construct machines that perform a desired function and have the desired property.

[mkleczek]

> It suffices that we can reliably construct machines that perform a desired function and have the desired property.

See above - there is no reliable procedure (algorithm) that would allow you to do that.