Smaller, cheaper Plutus scripts with the UPLC command-line tool (opens in new tab)

If you want to see a use of Agda in real life, to provide certificates validating the correctness of compiler passes, check out this blog post from my colleague Ziyang Liu at Input Output\. A simplified description of one of the passes appears in A Tale of Two Zippers, by myself, Jacco Krijnen, and Ramsay Taylor\.