The lambda calculus, developed by Alonzo Church in the 1930s, is a minimal but powerful model of computation based purely on function abstraction and application.

In lambda calculus, everything is a function. The only operations are:

1. Variable reference: x
2. Function creation (abstraction): λx.M
3. Function application: (M N)

Despite (or perhaps because of) this simplicity, the lambda calculus can express all computable functions. It forms the theoretical foundation for functional programming languages and has deep connections to both logic and mathematics through the Curry-Howard correspondence.

The Curry-Howard correspondence, also known as the proofs-as-programs correspondence, reveals a deep connection between computer programs and mathematical proofs.

This remarkable isomorphism shows that:

• Types correspond to propositions
• Programs correspond to proofs
• Program execution corresponds to proof normalization

For example:

• The type A → B corresponds to the logical implication A ⊃ B
• Product types (A × B) correspond to logical conjunction (A ∧ B)
• Sum types (A + B) correspond to logical disjunction (A ∨ B)

This correspondence has profound implications for both computer science and mathematics, suggesting that programming and mathematical proof are fundamentally the same activity viewed through different lenses.

Boolean algebra, developed by George Boole in the 19th century, provides the mathematical foundation for digital computing and logical reasoning.

The fundamental operations in Boolean algebra are:

• AND (conjunction)
• OR (disjunction)
• NOT (negation)

These simple operations, combined with the values True and False, form a complete system for logical reasoning. This system is not just theoretically interesting - it’s the basis for all digital computer operations, from simple calculations to complex decision-making algorithms.