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.
Reference
- Notes
- formal-logic, software-engineering, types
- 'Propositions as Types' by Philip Wadler
-
Permalink to
2023.NTE.630 - Edit