> This is I think is equivalent to proving that it is total implying it is primitive recursive?
No, as the article shows there are functions which terminate that aren't primitive recursive, and indeed Agda and (probably?) the others can prove termination for some (but necessarily not all) terminating non-primitive-recursive functions.
I think the misinformation that the article is complaining about is something like (my paraphrase):
> "Turing completeness" means "can do computation" while "non-Turing complete" means both "can't do computation" and "has nice configuration-language properties"
The article points out:
- you can be non-Turing complete and still do lots of computationally-expensive / tricky work
- your configuration language probably wants much stricter limits than merely being non-Turing complete
> I think the misinformation that the article is complaining about is something like (my paraphrase):
> > "Turing completeness" means "can do computation" while "non-Turing complete" means both "can't do computation" and "has nice configuration-language properties"
"Turing complete" means it can do any computation a Turing machine can. That is absolutely more power than is desired about 99.99% of the time. You almost always want your algorithms to contain no infinite loops.
(Algorithms. Not IO loops. Those are different, and the process of taking outside input while the program is running is outside the scope of what a Turing machine talks about anyway.)
Turing completeness is an ergonomics hack, and one with a decently successful history. But it's no panacea, and if we could find an ergonomic way to get rid of it, that would be a win.
Yes, even if we didn't also enforce primitive recursion. Sure, it's nice to know you're also not accidentally running Ackerman's function, but to be honest... I've had many more accidental infinite loops than accidental Ackerman's functions in my code. By approximately 10,000 to 0.
No system can ever prevent all errors. So let's focus on preventing the most common current ones.
First thing I do when I am learning a new high level language is write Ackermann function and see what happens. Also write out plus and mult and expt in terms of +=1. I have seen people with O(n^4) code when they could have easily used O(log n) but never seen an Ackermann in the wild.
No, as the article shows there are functions which terminate that aren't primitive recursive, and indeed Agda and (probably?) the others can prove termination for some (but necessarily not all) terminating non-primitive-recursive functions.
I think the misinformation that the article is complaining about is something like (my paraphrase):
> "Turing completeness" means "can do computation" while "non-Turing complete" means both "can't do computation" and "has nice configuration-language properties"
The article points out:
- you can be non-Turing complete and still do lots of computationally-expensive / tricky work
- your configuration language probably wants much stricter limits than merely being non-Turing complete