I have migrated my blog from Jekyll to the Lean programming language and the Verso documentation framework.

I prefer to use a typechecked programming language to write my blog.

This also means I can now include Lean proofs and formally verified code directly in my posts :-) I don’t expect to use this feature often, but here’s an example:

theorem example_identity (n : Nat) : n + 0 = n := n:Nat⊢ n + 0 = n All goals completed! 🐙