that creates some strange looking code in your desired goal language.
The code wouldn’t just look strange, it would likely be more complex than code written directly in the language using its standard style at a high level to solve the same problem. The reversed compiled code would be harder to analyze, and harder to know what would be useful to prove about it, than code written directly in the target language with the reasoning behind why the programmer expects it to work serving as a guide to construct the proof.
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.
The code wouldn’t just look strange, it would likely be more complex than code written directly in the language using its standard style at a high level to solve the same problem. The reversed compiled code would be harder to analyze, and harder to know what would be useful to prove about it, than code written directly in the target language with the reasoning behind why the programmer expects it to work serving as a guide to construct the proof.
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.