So Phillip Wadler and Wen Kokke released a new book on Programming Language Foundations In Agda, and it just so happens that the Plutus Metatheory was written in Agda as well (which comes as no surprise since Wadler is part of the project/if not leading it).
Thus if you are into PL theory, dependent types, and/or theorem proving, now’s not a bad time to learn some more:
The book: https://plfa.github.io/
Plutus Metatheory repo: https://github.com/input-output-hk/plutus-metatheory