I've got interested in formalization of mathematics recently and found the book Type Theory and Formal Proof by Nederpelt and Geuvers is a really nice one, taking you from the untyped lambda calculus and gradually extending the type system until you get the full dependent type theory and the Calculus of Constructions that underlies, e.g., the Lean language/proofchecker

Peter Smith (logic God) also recommends it in his logic study guide:

https://www.logicmatters.net/tyl/

I really like combinatory logic and lambda calculus, and I think it should be used to define common semantics for various languages and computer systems.

Lately, I was wondering about if it's possible to represent any logic by choosing a suitable base of combinators, and the sentences in the logic would correspond to beta-normal terms expressed in those combinators. What brought me to the idea is that we can represent certain substructural logics using a subset of B, C, K, W. Also, one can represent classical logic by using a different base than S and K, which allows for call/cc.

What would be intriguing, a choice of combinator base such that it could express terms in Church's typed lambda calculus. The composition of combinators would fail to normalize iff the corresponding composed term in typed lambda calculus failed to typecheck.

I think this could lead to somewhat simpler foundations of mathematics, instead of having types and various axioms, we would just say here's a base set of combinators and have fun combining them.

500