![Propositions in logic correspond to types in a programming l...](https://i.ytimg.com/vi/IOiZatlZtGU/hqdefault.jpg?sqp=-oaymwEjCNACELwBSFryq4qpAxUIARUAAAAAGAElAADIQj0AgKJDeAE=&rs=AOn4CLABaNUeCwNiUQhFxigSLPfSeE3XAQ)
Propositions in logic correspond to types in a programming language.
Proofs in the logic correspond to terms and programs in the programming language
Simplification of proofs corresponds to evaluation of programs.
The program is a path to solving a proof - to proving a statement correct or incorrect.
Josh Beckman