re: the argument, not mine, they explained it somewhere else, albeit it is hard to get.
By in practice, I mean in anything that haven’t got computing power substantially larger than that of the universe. You don’t feed the tail into the dragon when your dragon has finite mouth and long tail, that is to say, you dont feed source code into theorem provers if you don’t have to; instead you actively try to simplify the stuff that is being processed by theorem prover. You don’t make equivalence of your code with provisional output an axiom, you make it a substitution rule that works one way (it still makes nonsense eventually, but easily long after all the stars in the universe have burnt themselves out, and that can too be fixed). That is assuming you are using state of the art automated algebra package to implement decision theory.
re: the argument, not mine, they explained it somewhere else, albeit it is hard to get.
By in practice, I mean in anything that haven’t got computing power substantially larger than that of the universe. You don’t feed the tail into the dragon when your dragon has finite mouth and long tail, that is to say, you dont feed source code into theorem provers if you don’t have to; instead you actively try to simplify the stuff that is being processed by theorem prover. You don’t make equivalence of your code with provisional output an axiom, you make it a substitution rule that works one way (it still makes nonsense eventually, but easily long after all the stars in the universe have burnt themselves out, and that can too be fixed). That is assuming you are using state of the art automated algebra package to implement decision theory.