Lisp? Meh! The real secret is Agda.<p>The real real secret is using a language so obscure that you end up writing the compiler for production use, by studying the compiler that some researcher created for a paper.