Programming Language Fundamentals in Agda
15 points by solomon
15 points by solomon
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.
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!
Thanks, I didn't know about this book in particular. I first learned the basics of mechanization from Pierce's Software Foundations series (after previously learning the basics of programming language theory from his textbooks) and I think they're still an excellent resource even if you're not using Rocq: https://softwarefoundations.cis.upenn.edu/. When I started learning Lean a few years ago, I more or less just redid the first few volumes in Lean, and most of it was a straightforward translation; I guess redoing it in Agda would be a bigger undertaking.
There are also excellent (free) books for Isabelle. In general I've found that it's not too onerous to adapt these kinds of intro-level works to other proof assistants, and it's helpful to at least learn enough of all the major systems to benefit from publications that rely on them. [1]
[1] The only widely used systems whose code I find totally inscrutable, despite or maybe because of the simplicity of their logical foundations and trusted computing base, are the HOL family. The CakeML project has produced some of the best work in recent years on certified compilers and seL4 was obviously an important milestone in certified systems software; I've read all their papers but I wish I could actually make much sense of their proof code.
I went through this book during covid. Highly recommend. Especially if you have no background in PL or logic the first chapter is very edifying and agda is a good choice due to its mixfix operators