I believe Rice’s theorem applies to a programmable calculator. Do you think it is impossible to prove that a programmable handheld calculator is “safe”? Do you think it is impossible to make a programmable calculator safe?
My point is, just because you can’t formally, mathematically prove something, doesn’t mean it’s not true.
You can formally mathematically prove a programmable calculator. You just can’t formally mathematically prove every possible programmable calculator. On the other hand, if you can’t mathematically prove a given programmable calculator, it might be a sign that your design is an horrible sludge. On the other other hand, deep-learnt neural networks are definitionally horrible sludge.
I think halting undecidability and Rice’s theorem are being misapplied here.
It is true that no algorithm can determine, for every possible program and input, whether that program will halt. But for specific programs and inputs, it is often possible to figure out whether they halt or not.
I agree that there is no method that allows us to check all possible AGI designs for a specific nontrivial behavioral property. But this does not forbid us to select an AGI design for which we can prove that it has a specific behavioral property!
Does Rice theorem resolve the halting problem?
I believe Rice’s theorem applies to a programmable calculator. Do you think it is impossible to prove that a programmable handheld calculator is “safe”? Do you think it is impossible to make a programmable calculator safe?
My point is, just because you can’t formally, mathematically prove something, doesn’t mean it’s not true.
You can formally mathematically prove a programmable calculator. You just can’t formally mathematically prove every possible programmable calculator. On the other hand, if you can’t mathematically prove a given programmable calculator, it might be a sign that your design is an horrible sludge. On the other other hand, deep-learnt neural networks are definitionally horrible sludge.
I think halting undecidability and Rice’s theorem are being misapplied here. It is true that no algorithm can determine, for every possible program and input, whether that program will halt. But for specific programs and inputs, it is often possible to figure out whether they halt or not.
I agree that there is no method that allows us to check all possible AGI designs for a specific nontrivial behavioral property. But this does not forbid us to select an AGI design for which we can prove that it has a specific behavioral property!