As Coq approaches 35 years of history, the development of interactive proofs is more relevant than ever; crucial correctness properties can only be established mechanically with the help of humans, and the challenges that users and tooling face in the context of large-scale proofs are still considerable.

In this talk, I will try to explore Coq user interfaces from 3 different perspectives: first, we will survey past work. Many great ideas have been proposed over the years, however, implementation and maintenance have not always been a path of roses.

Understanding areas in need of improvement will lead us to the second part of the talk, where I will present SerAPI.

SerAPI aims to be a state-of-the-art language server for the Coq ecosystem. Special care has been put into its design to prevent maintenance and robustness problems. SerAPI provides an API for building and querying Coq documents, and has been successfully used by several projects.

While SerAPI works reasonably well today, is far from being a mature language server. In the final part of the talk, we will examine ongoing and future tooling work in the SerAPI/Coq roadmap. Some key issues are project management, incremental compilation, feature extraction, a enhanced display model, and support of standards such as the Language Server Protocol.