[TYPES] What's a program? (Seriously)

[Andrew Polonsky]

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