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’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.