Research

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.