Is this in any way related to Software Foundations Volume 2: Programming Language Foundations [0] (in Coq)? The table of contents looks quite different but the choice of name suggest some commonality.

[0] https://softwarefoundations.cis.upenn.edu/plf-current/toc.ht...

Wadler stated in a talk somewhere that he was inspired by that book, but thought Agda may be more approachable.

The second paragraph of [0] says about the same, with reasons.

[0]: https://plfa.github.io/Preface/#personal-remarks

Here’s a runnable version of this book https://nextjournal.com/try/plfa/Naturals

It’s been very difficult for me to devote any time to dependent type theory and it’s associated programming languages. It seems incredibly complicated for fairly little gain, since mis-specifying programs is so common.

I’m much more fond of the TLA+ style thinking of using simple untyped set theory and model-checking to verify computations.