wedrifid comments on GAZP vs. GLUT - Less Wrong
You are viewing a comment permalink. View the original post to see all comments and the full post content.
You are viewing a comment permalink. View the original post to see all comments and the full post content.
Comments (166)
I don't think we even need turing-completeness, really. Take a total language, and give it a loop-timeout of say 3^^^^3. It can compute anything we care about, and is still guaranteed to terminate in bounded time.
(I'm reminded of Godel's letter discussing P=NP - should such an algorithm be found, mathematicians could be replaced by a machine that searches all proofs with less than a few million symbols; anything that couldn't be proved with that many symbols would be of little to no interest to us.)
Or, at least, they could be replaced by people who can understand and seek out proofs that are relevant to us out of the arbitrarily large number of useless ones. So mathematicians basically.