Other content
Posts
-
Writing Technical Posts in Lean
I've been thinking about starting a technical blog for a while, and recently decided to try Verso—a documentation tool that lets you write in Lean 4. The appeal is being able to mix explanations with actual executable code and verified proofs rather than relying on screenshots or hand-wavy arguments. Since Lean understands the code directly, you get accurate syntax highlighting, identifiers automatically link to the Lean reference manual, and you can hover over functions to see their documentation and type signatures.
Here are a couple of examples to show what this looks like in practice.
Read more -
Starting This Blog
I've been meaning to start writing about technical topics for a while, but kept putting it off. The usual blogging platforms never felt quite right for the kind of content I wanted to create—mixing code examples with mathematical reasoning in a way that actually works.
Over the past year, I've been learning about formal methods and theorem proving, partly out of curiosity and partly because I think these techniques could be useful for writing more reliable software.
Read more