Scrap Your Boilerplate

12 lines of Agda code is verified red-black tree insertion.
12 lines of Java code would be a class declaration with some getters/setters

Lisp macros can be done with just a couple of Haskell libraries, and in a type-safe way

http://stackoverflow.com/questions/24172117/navigating-and-modifying-asts-built-on-the-free-monad-in-haskell