[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
I would argue that every proof is a program which takes as input evidence that the hypotheses of a given statement are true, and produces as output evidence that the conclusion is true. This is the essence of the BHK interpretation, but is equally valid when considered for classical systems like ZFC, NGB, ZFC+Vopenka cardinal, etc. The machine running such a program though is not a Turing Machine, or some reduction system, but is the human mind. The proof/program can be presented with different levels of precision: as a sketch/flowchart, informal/pseudocode, a formal script in a particular logic/language, or fully formalized/compiled. Different machines will generally require different layers of precision in order to be able to "run" a given proof (i.e., to understand it). On the other hand, I don't see how every program can be considered a proof. What does the following program prove, for example? https://www.ioccc.org/1984/mullender/mullender.c Perhaps it proves my point. ;) But that is not immanent in the program itself. (And I am certain that some will disagree.) Best, Andrew
