tl;dr: String diagrams are an intuitive diagrammatic representation of some pretty useful math. This being Interactive Theorem Proving, of course, I want to formalize that math in a proof assistant (Coq), in such a way that formal proofs still work like paper proofs using all the nifty properties of the diagrammatic representation. And, of course, a naïve formalization runs into problems that make the system painful to use. So this project explores how we might overcome those problems and restore the convenience of string diagrams in a formal setting.

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.

Let's say you've written a programming language in Coq. You have nice inductives for your ASTs; one for untyped terms (UntypedAST) and one for typed terms (TypedAST). You wrote a simple typechecker, and maybe an interpreter, too!

typecheck
     : UntypedAST -> option TypedAST
interp
     : TypedAST -> Value

You write a few programs…

Example well_typed := UAdd (UNat 1) (UNat 1).
Example ill_typed := UAdd (UNat 1) (UBool true).

… typecheck them:

Definition tc_good := typecheck well_typed.
Compute tc_good. (* Accepted: So far so good. *)
= Some
    {|
    tau := Nat;
    ast := TAdd (TNat 1) (TNat 1) |}
: option TypedAST

Definition tc_bad := typecheck ill_typed.
Compute tc_bad. (* Rejected: all good as well. *)
= None
: option TypedAST

… and attempt to run them:

Compute interp tc_good.
The term "tc_good" has type "option TypedAST"
while it is expected to have type "TypedAST".

D'oh! interp takes a TypedAST, but typecheck returns an option. What do we do?

A fairly common occurrence when working with dependent types in Coq is to call Compute on a benign expression and get back a giant, partially-reduced term, like this:

Import EqNotations Vector.VectorNotations.
Compute (Vector.hd (rew (Nat.add_1_r 3) in ([1; 2; 3] ++ [4]))).
= match
    match
      Nat.add_1_r 3 in (_ = H)
      return (Vector.t nat H)
    with
    | eq_refl => [1; 2; 3; 4]
    end as c in (Vector.t _ H)
    return
      (match
         H as c0 return (Vector.t nat c0 -> Type)
       with
       | 0 =>
           fun _ : Vector.t nat 0 =>
           False -> forall x1 : Prop, x1 -> x1
       | S x => fun _ : Vector.t nat (S x) => nat
       end c)
  with
  | [] =>
      fun x : False =>
      match
        x return (forall x0 : Prop, x0 -> x0)
      with
      end
  | h :: _ => h
  end
: (fun (n : nat) (_ : Vector.t nat (S n)) => nat)
    3
    (rew [Vector.t nat] Nat.add_1_r 3 in
     ([1; 2; 3] ++ [4]))

This post shows how to work around this issue.