Proofs as programs (Was: Advent of Logic 2024: Weekend 3)

On 14/12/2024 22:13, Mild Shock wrote:

Create a proof search in Simple Types,
that finds Lambda Expressions as proof,
for a given formula in propositional logic.

Thinking about it:
Either by hand or with a 'solve', we/I [*] go from a Goal to a Proof (proof tree).  And, by Curry-Howard, that is (already!) our Type and witnessing Term, i.e. our Proof is a program whose type is the Goal. Indeed, we also already find type-checking: of a Proof against the Goal it alleges to be a proof of.
What program does the Proof represent?  If a Goal is of the form `G=>Z`, where `G` is the context (some collection of Formulas as hypotheses), and Formula `Z` is the conclusion, we interpret a Goal as a function from the hypotheses to the conclusion.
To execute a Proof we need a "machine", namely, a function 'eval' that takes the Proof as well as witnessing Terms for each hypothesis, and returns a Term witnessing the conclusion.  (Which also requires a system of Terms: but I am not yet sure about the details...)
More than that, we can 'compile' the Proof to some target language (the system's host language being the first candidate), to produce a function in the target language that is like 'eval' except specialized to the given Proof as well as to as many hypothesis Terms as can be fixed...
Sounds good?  Anything else?  :)
-Julio
[*] See <https://gist.github.com/jp-diegidio/b6a7a071f9f81a469c493c4afcc5cb11#file-gentzen-pl>