Soundness, Completeness, and some Philosophy

Slides for the video (at the end).

Proofs as Programs, Propositions as Types

As mentioned in the video, there is a possible interpretation of logical proofs as processes transforming evidence from premises to conclusions.

One way of taking this idea further is to build an entire combined programming and proving system based on the slogans “Proofs as Programs” and “Propositions as Types”. This close connection is sometimes called the Curry-Howard correspondence (or, less correctly, isomorphism), after the logicians Haskell Curry and William Alvin Howard.

The video Propositions as Types by Prof. Phil Wadler (see also the paper) describes the idea in an accessible way.

If you do the CS410 Advanced Functional Programming course in 4th year, you will explore the Agda system which implements this idea to make writing proofs and programs the same activity.