On several occasions, the authors emphasize how the intuitive nature of “effective computability” renders futile any attempt to formalize the thesis. However, I’m rather interested in formalizing intuitive concepts and therefore wondered why this hasn’t been attempted.
Formalizing the intuitive notion of effective computability was exactly what Turing was trying to do when he introduced Turing machines, and Turing’s thesis claims that his attempt was successful. If you come up with a new formalization of effective computability and prove it equivalent to Turing computability, then in order to use this as a proof of Turing’s thesis, you would need to argue that your new formalization is correct. But such an argument would inevitably be informal, since it links a formal concept to an informal concept, and there already have been informal arguments for Turing’s thesis, so I don’t think there is anything really fundamental to be gained from this.
Another way of putting it: you can’t possibly know that there isn’t some device out in the universe that lets you do more powerful things than your model (eg. a device that can tell you whether an arbitrary Turing machine halts), so it can never be proven that your model captures real-world computability.
Formalizing the intuitive notion of effective computability was exactly what Turing was trying to do when he introduced Turing machines, and Turing’s thesis claims that his attempt was successful. If you come up with a new formalization of effective computability and prove it equivalent to Turing computability, then in order to use this as a proof of Turing’s thesis, you would need to argue that your new formalization is correct. But such an argument would inevitably be informal, since it links a formal concept to an informal concept, and there already have been informal arguments for Turing’s thesis, so I don’t think there is anything really fundamental to be gained from this.
Another way of putting it: you can’t possibly know that there isn’t some device out in the universe that lets you do more powerful things than your model (eg. a device that can tell you whether an arbitrary Turing machine halts), so it can never be proven that your model captures real-world computability.
Be careful stating what physics can’t prove.
Fwiw, I disagree with the frame of that post as well.
I’m happy to agree that you can prove that your model captures real-world computability under a particular formalization of physics.