Interactive theorem provers like Coq, Agda and Idris allow programmers to ask questions about incomplete programs (or proofs) to Emacs, and get meaningful answers based on types of the missing parts. This turns programming into a conversation between programmers and their compilers, where Emacs acts as an intermediary. However, programmers are limited in the kinds of questions they can ask. Recent work on extensible editor actions leverages metaprogramming techniques to specify how the compiler should answer custom questions, but that requires writing code in Emacs Lisp to glue the compiler and the editor interface because metaprograms can only command the compiler and not the editor itself.

In this talk, I will describe editor metaprogramming, a novel idea of writing metaprograms that command the editor. I define a monadic embedded domain-specific language (eDSL) for editor commands in Coq, which enables composing these commands in meaningful ways, with the full power of Coq! I will write an interpreter for this eDSL in Emacs Lisp, and make Emacs and Coq processes communicate back and forth. Coq computations will be sent back to Coq, and effectful editor actions such as deleting a character and moving the cursor will be executed in Emacs Lisp.