Yes, however from what I recall about such proving methods, they were quite formulaic and about an equal amount of pain for each line (I should dig out some references some time), so the difference may not be as pronounced. Be that as it may, I agree that there is a difference in degree, which does matter for practical purposes.
I expect it is more than a difference in degree. When the programmer can tell the automated theorem prover that the return value of a certain function always satisfies some condition that other functions rely on, the theorem prover can try to prove that condition holds and use that fact for other proofs without being distracted by other possible conditions that are not relevant. This makes the search space much smaller.
The point is that the programmer having some understanding of the proof checker, and designing the code to be not just correct, but provably correct in a reasonable amount of time makes a big difference from the general problem of proving things about arbitrary code where you run into the halting problem.
I agree with both your example (“making the search space much smaller”) and your explanation (“makes a big difference”), we just differ on whether thus changing the resource requirements constitutes a change in kind, or one in degree.
Also, I took your “code would likely be more complex” as “be less human-understandable”, as opposed to its actual Kolmogorov complexity, which afaik would be identical.
Yes, however from what I recall about such proving methods, they were quite formulaic and about an equal amount of pain for each line (I should dig out some references some time), so the difference may not be as pronounced. Be that as it may, I agree that there is a difference in degree, which does matter for practical purposes.
I expect it is more than a difference in degree. When the programmer can tell the automated theorem prover that the return value of a certain function always satisfies some condition that other functions rely on, the theorem prover can try to prove that condition holds and use that fact for other proofs without being distracted by other possible conditions that are not relevant. This makes the search space much smaller.
The point is that the programmer having some understanding of the proof checker, and designing the code to be not just correct, but provably correct in a reasonable amount of time makes a big difference from the general problem of proving things about arbitrary code where you run into the halting problem.
I agree with both your example (“making the search space much smaller”) and your explanation (“makes a big difference”), we just differ on whether thus changing the resource requirements constitutes a change in kind, or one in degree.
Also, I took your “code would likely be more complex” as “be less human-understandable”, as opposed to its actual Kolmogorov complexity, which afaik would be identical.