The Little Typer

Daniel P. Friedman is famous for his "Little" series of books. Little Schemer, Little prover, Little MLer and so on. These books are held in high regard. Dan's coauthor is David Thrane Christiansen, Idris contributor, and host of a podcast about type theory that is way over my head. Together they are going to teach us how the programming skills we already have can be used to develop rigorous mathematical proofs.