Programming languages, type theory, OCaml & Lean
Interactive Lean proofs with hoverable goal states, via LeanInk + Alectryon.
Rebuilding the blog on Quarto.
A test post exercising math typesetting and OCaml highlighting.