Code Generation via Meta-programming in Dependently Typed Proof Assistants

Abstract Dependently typed proof assistants offer powerful meta-programming features, which allow users to implement proof automation or compile-time code generation. This paper surveys meta-programming frameworks in Rocq, Agda, and Lean, with seven implementations of a running example: deriving instances for the typeclass. This example is fairly simple, but realistic enough to highlight recurring difficulties with meta-programming: conceptual limitations of frameworks such as term representation – and in particular binder representation –, meta-language expressiveness, and verifiability, as well as current limitations such as API completeness, learning curve, and prover state management, which could in principle be remedied. We conclude with insights regarding features an ideal meta-programming framework should provide.