I wrote a C0 (subset of C) to Wasm compiler in #Lean4 that can be ran in the browser. You can try it out here: https://theabrick.com/c0/
While the end goal is to completely verify it, only part of that is completed as of right now.
I am also working on tooling and other somewhat tangential features. One of these tools that I wrote that was particularly cool/interesting is a Lean inductive definition to LaTeX'd inference rule converter.
Essentially you can encode inference rules in Lean (see first image) and with minimal configuration, the tool will output a corresponding typeset inference rule (see second picture). I've posted the static semantics that I've been able to generate for C0 so far here: https://theabrick.com/c0/statics.pdf
I see this having a couple of benefits. Number one being that I think it is much easier to double check inference rules for correctness than to read lines of code (and likewise the reader doesn't need to know Lean to understand the rules). I also find typesetting inference rules to somewhat difficult and tedious, but writing them in Lean is much easier (likewise this also removes potential typos between the two different versions of the rules).
I still need to flesh out and cleanup the converter before I would consider it generally usable. I just couldn't resist showing it off right now though : ) Hopefully I will have it finished soon!
