Zettelkastens and Literate Programs

I've been re-reading John Harrison's Handbook of Practical Logic and Automated Reasoning (a wonderful book), with an eye towards writing notes for my Zettelkasten.

What I have done, out of habit, is I've reworked the code in Standard ML (as opposed to OCaml). I've added a "register" (mathematicians would recognize them as "theorem environments" in LaTeX) for source code, and the template for writing such notes on a 5.5 inch by 4.25 inch (A6) slip of paper looks like:

[id number]		Code [name of chunk]
[English summary of the code, or the algorithm, or...]
⟨[name of chunk]⟩≡
[Standard ML code here]

Just replace the bracketed italicized text (including the brackets) with your own text. I do write a horizontal line separating the "code block" from the "text block", and underline the "Code" part of the title.

I follow the general heuristics Knuth suggests for literate programming, even using the names of code chunks in angled braces as if they were statements. Following some of the early handwritten documents on Standard ML, I underline keywords like "if", "then", "else", "case", "fun", etc., in the code block.

While reading Harrison's book, I add unit tests, write up examples, etc. This isn't done "in the abstract", I actually type the code up on a computer (e.g., here is my implementation of most of the propositional logic code).

One advantage to this is that we can prove properties about the code snippet in branches off the code zettel. Another advantage, giving a good human-level summary of the code snippet helps greatly with Harrison's book, since the techniques from chapter 3 make another appearance in chapter 6 (i.e., 300 pages later) and I forget some of the nuances surrounding the implementation ("Is skolem called before or after nnf?"), I can just glance at the snippets for guidance.

Another useful aspect of using a Zettelkasten for studying theorem provers is that it facilitates blending notes from multiple books seamlessly. I noticed this accidentally, when I was unsatisfied with Harrison's description of Herbrand universes, then started reading Chang and Lee's Symbolic Logic and Mechanical Theorem Proving (1973) description of Herbrand universes.

There are other aspects of Zettelkasten which seems uniquely suitable for studying theorem provers, but I digress.

I'm experimenting with using a Zettelkasten for literate programming "by hand" more generally, which is a bizarre but fascinating experience, especially when exploring monads in Standard ML.

Anyways, I just wanted to make note of this quirky note-taking system for literate programming.