The connection between logic and computation runs deep, from the Curry-Howard correspondence to automated theorem proving.

Understanding how proofs correspond to programs, and vice versa, sheds light on both fields. This note is a stub—expand with your own observations and links.