After a decade of neglect, the old Jekyll site is gone and this blog now runs on Quarto.
The plan for what lives here: programming languages, type theory, and proof assistants — with code in OCaml and proofs in Lean, plenty of mathematics, and the occasional digression.
Posts render to HTML with live math, and can also be exported to PDF when a typeset version is useful.