Josh

Building in the open

Note on 'Propositions as Types' by Philip Wadler via Strange Loop Conference

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.

Keyboard Shortcuts

Key Action
o Source
e Edit
i Insight
r Random
h Home
s or / Search
www.joshbeckman.org/notes/629405755