Mechanizing formal systems and proofs about them plays an important role in establishing trust in programming languages and verifying software systems in general. Over the past decades, we have seen significant progress and success: the POPLMark challenge popularized the use of proof assistants in mechanizing the metatheory of programming languages; the development of the first verified compiler in Coq demonstrated the feasibility and value of building verified compilers. Today, mechanizing proofs is a stable fixture in the daily life of programming languages researchers.

One might be tempted to assume that all is well – yet, the reality is that we seem to accept the status quo and focus on engineering solutions to get the next job done, although mechanizations can be time consuming and require substantial (sometimes heroic) effort. In this talk I will argue that we should strive to develop high-level abstractions, primitives, and tools to standardize common tasks and operations arising when working with formal systems and proofs about them.

Taking a look back at some of the foundational theoretical ideas and choices that underly type-theoretic proof environments today, I will survey recent achievements and sketch a dependently typed language that would make it easier to represent, maintain, and communicate formal systems and proofs about them – an elegant proof language for a more civilized age.