Turing completeness as the ultimate measure of expressiveness for programing/logical systems is a myth. I argue every interesting program you may want to write

Turing completeness as the ultimate measure of expressiveness for programing/logical systems is a myth. I argue every interesting program you may want to write is either terminating, co-terminating or step-indexed. Terminating programs are well understood (using structural recursion, inductive data, etc). Co-terminating programs are stuff like servers/daemons/guis: you want them to (possibly) never terminate and always progress (respond) in finite time, these are expressible using coinductive data, structural corecursion etc. And lastly, if you have a program which may hang for an indefinite amount of time, you really should put a timeout (or heck, a co-timeout, eg some kind of heartbeat), that's step-indexing. So no, Coq and other "total" programing languages (agda, idris, F*) may not be turing complete in the usual sense because the two things are contradictory, but they are much better: you can simulate a turing machine as a server which will be provably always making progress in finite time. See this paper for some more insights: https://personal.cis.strath.ac.uk/conor.mcbride/TotallyFree.pdf https://personal.cis.strath.ac.uk/conor.mcbride/TotallyFree....