Given the explosion of interest in proof checkers recently I thought it would be good to promote PLFA. This is an online book that walks you through the basics of logic, programming language design, and formalization using Agda.

I think many people here might be surprised by what writing proofs in Lean/Agda/Rocq/Idris is actually like.

If you have only seen a giant wall of proof output from an LLM then it probably looks like writing some kind of alien "assembly language for math." This couldn't be further from the truth. These are very high level functional languages with sophisticated developer tooling.

Working with a proof checker does more then help you understand the thing you are proving. It teaches you about abstraction, software design, and type theory. I strongly believe this makes you a better software engineer. Its also surprisingly fun and game like!