In the past few months, I have been using the Lean 4 proof assistant for formalising programming language semantics and safety properties in my HDL line of research (e.g., Anvil). I would like to share my thoughts and experience regarding the use of Lean in this blog post.
Where It Helps Lean is a proof assistant so of course we expect it to assist.
One obvious way it helps is that once I write down some proof in Lean, it can type-check it to see if it is correct.
I’ve been trying Typst in my work for some time. For those of you who don’t know, Typst is a new language/tool for typsetting technical documents. Its goal is to be a better alternative to (La)TeX, which as probably everyone in the academia would agree, has not been pleasant to use. Different people might have different problems with LaTeX. For me, it’s mostly the gibberish error messages (such as “Undefined control sequence” followed by some weird string I’ve never seen), confusing package compatibility (some package for some reason can’t be used together with a package in the dependencies of acmart?