I anticipated and addressed the objection around Rice’s theorem (without calling it that) in a child to my first comment, which was published 16 min before your comment, but maybe it took you 16 min to write yours.
A better way of making your argument might be to suggest that entity that was better at programming would have intentionally constructed a program that it knew was safe to begin with, and therefore had no need of simulation, rather than that it could just inspect any arbitrary program and know that it was safe.
I was assuming the reader would be charitable enough to me to interpret my words as including that possibility (since verifying that a program has property X is so similar to constructing a program with property X).
I’m sorry to have misjudged you. Possibly the reason is that, in my mind, constructing a program that provably has property X, and in the process generating a proof, feels like an almost totally different activity from trying to generate a proof given a program from an external source, especially if the property is nontrivial.
I anticipated and addressed the objection around Rice’s theorem (without calling it that) in a child to my first comment, which was published 16 min before your comment, but maybe it took you 16 min to write yours.
I was assuming the reader would be charitable enough to me to interpret my words as including that possibility (since verifying that a program has property X is so similar to constructing a program with property X).
I’m sorry to have misjudged you. Possibly the reason is that, in my mind, constructing a program that provably has property X, and in the process generating a proof, feels like an almost totally different activity from trying to generate a proof given a program from an external source, especially if the property is nontrivial.
I agree with that, for sure. I didn’t point it out because the reader does not need to consider that distinction to follow my argument.