> Every program can be made into a proof

I'm not sure what you mean by this, but in my usage it's exactly the other way around. A proof can easily be interpreted as a program (as per the BHK and similar interpretations) but to interpret a program as a proof of something, you at least need to also formally prove that it halts. Edit: your edit clarified things a bit. The control flow in formal (and informal!) proofs is restricted compared to the control flow in programs: in order to do recursion or loops, you must have a formal argument that the recursion / loop terminates.

So normally when we say "proof", we assume the proof is correct. But in this discussion we are talking about possibly incorrect proofs, with the goal of verifying the correctness of the proof. So let's change "proof" to set of statements/procedures which may evaluate to "true", and we need to verify that they do evaluate to true. Things like loops do appear in proofs as quantifiers. So for example a proof may perform a sequence of steps in which some set is depleted, and conclude that "as we must deplete all the elements the set, the claim holds", but determining whether all elements are actually depleted by the algorithm spelled out in the proof may be hard. These types of claims appear in actual proofs, and the types of errors that are found in proofs often boil down to some case being not considered which would cause the set not to be depleted.

Update: I'm unable to reply due to hn recursion limits, but as to your strictly smaller argument, that is not enough with infinite sets, which are common in proofs. Consider a proof about all surfaces, which you think you divided into a countable number of cases, but in reality there are some other types of surfaces you haven't considered. In math you are making assertions, in some sense, about the world, albeit the mathematical world, and you are claiming to have explored all the relevant parts of it for the sets of interest, but you may have not explored some parts you didn't know existed. The idea that you can formally verify such a sequence of claims is .. mind boggling. There is a reason why very little progress has been made in formalizing math, and mistakes are sometimes discovered in even published proofs.

This is all a bit vague, so I may be misinterpreting here. But in the given example, the proof must also prove that at each step the set is getting strictly smaller, so the computer still only has to check that the proof is correct. That is, it doesn't have to check for itself whether the set is getting smaller, it just asks you to prove that the set is getting smaller in a way that it understands.

Anything more fancy than that is left up to proof automation, which is free to give up and say "nope, that leap's too big for me."

> So let's change "proof" to set of statements/procedures which may evaluate to "true", and we need to verify that they do evaluate to true.

I'm not sure that's a good way of looking at it. I think the right image is to think of a proof as a program, and checking the proof as typechecking the program. The program has the additional restriction that whenever it does loops or recursion, it has to prove that something is getting strictly smaller with each iteration.

Wrt your update,

> The idea that you can formally verify such a sequence of claims is .. mind boggling.

Eh, if you're convinced that something's correct, it's not too mind-boggling that you can also explain it to a computer, given that it accepts all the same basic assumptions that you do.

> There is a reason why very little progress has been made in formalizing math, and mistakes are sometimes discovered in even published proofs.

Yep: it looks like Lean is making good progress on their goal of formalizing the "undergraduate curriculum," but that's only the tiniest sliver of math. Math is hard, and doing it formally is even harder, so all I'm saying is that contrary to your earlier statements, it's definitely possible.