The Cardano blockchain is the first to use proof of stake, offers native support for multiple currencies and is evolving toward a distributed governance model. It supports smart contracts through Plutus, a language based on System F$_\omega$ with recursion. About half a dozen languages compile into Plutus, the first of which is \emph{Plinth} (formerly Plutus Tx) — a subset of Haskell in commercial use since 2021.

Our journey building Plinth has been unconventional in a number of ways. First, Plinth is a subset of Haskell rather than a traditional embedded DSL, which brings a number of advantages. Second, compilation is primarily handled by a GHC plugin, one of the most intricate we are aware of. Third, while some compiler optimizations mirror those in Haskell, others diverge significantly to meet on-chain execution constraints. Fourth, Plutus programs run on an instrumented CEK machine with a formal specification in Agda. This report reflects on our design choices, outlining effective practices, challenges, and key takeaways, with an emphasis on recent advances in the language, compiler, and runtime.