If you're ever written small to moderately large Rocq developments, it's quite likely that you have experienced the following problem:

• You write your proofs using induction or case analysis, carefully making sure to list all (important) cases one by one.
• Later, as your project naturally grows, you decide to add a new case (a new typing rule, a new kind of expression, etc.).
• Suddenly, all proofs that you've written break, usually with no clear indication as to where and why the proof broke.

If this sounds familiar, you've bumped into one of the current pitfalls of goal selection: goals selectors such as bullets and numbers do not match constructors one-to-one (they lack a semantic connection to the constructor they're supposed to apply to).

I'll show in this post how we can improve the experience by automatically generating goal names, yielding a robust and future-proof method of selecting goals.

Specifications (such as RFCs, programming language standards) are typically written in natural language. To formally verify an implementation of such a spec, we need two things: a mechanization of the spec (in a theorem prover like Coq, Lean, Dafny, …), and a proof of correctness relating the implementation to the mechanized spec.

The correctness of the proof is guaranteed by the theorem prover. But who checks the correctness of the mechanization? The original spec is in natural language, so the best we can do is an audit. To make these audits easier, some specs are written in a “literate” style, with comments from the spec interleaved throughout the mechanization. This helps a lot, but… who checks the comments? In this post, I present SpecMerger, a tool that checks that literate comments match the spec they came from.

Alectryon (named after the Greek god of chicken) is a collection of tools for writing technical documents that mix Coq code and prose, in a style sometimes called literate programming.

Coq proofs are hard to understand in isolation: unlike pen-and-paper proofs, proof scripts only record the steps to take (induct on x, apply a theorem, …), not the states (goals) that these steps lead to. As a result, plain proof scripts are essentially incomprehensible without the assistance of an interactive interface like CoqIDE or Proof General.

The most common approach these days for sharing proofs with readers without forcing them to run Coq is to manually copy Coq's output into source code comments — a tedious, error-prone, and brittle process. Any text that accompanies the proof is also embedded in comments, making for a painful editing experience.

Alectryon does better: it automatically captures Coq's output and interleaves it with proof scripts to produce interactive webpages, and it lets you toggle between prose- and code-oriented perspectives on the same document so that you can use your favorite text editing mode for writing prose and your favorite Coq IDE for writing proofs.

Most PL conferences moved online this year, and many are asking authors to pre-record talks to avoid livestreaming difficulties. Here are the steps we followed to record and edit our Kôika talk at PLDI 2020 and our extraction talk at IJCAR 2020. This posts covers preparing and recording the talk, adding the slides, and captioning the final video.