Remember the Curry-Howard isomorphism?

Proofs are programs!

• Programs are usually constructed manually.

How do we manage complexity in programs?

1. We invent useful abstraction and construct libraries of reusable software components.
2. We use high-level languages with good abstraction mechanisms.
3. We make use of program generators (automation) for certain specific tasks (e.g. parsers).