WebAssembly spec in Lean4

Stream: general

[Joachim Breitner]

As some of you might know, the WebAssembly language has been co-developed with its formal spec, and this subsequently has been mechanized in Isabelle and then Coq. So far, the three artifacts (formal prose spec, formal math spec, Isabelle, Coq) have to be kept in sync manually. To improve this the people behind WebAssembly started to build a tool that generates these artifacts from a common source of truths.

Over the Easter holidays, I had fun targetting, as the _first_ theorem prover backend of this tool, Lean4, and it is now “essentially complete” with regard to the current (incomplete) input spec of this (still very WIP) tool. This is the current output:

https://github.com/Wasm-DSL/spectec/blob/joachim/spectec/test-lean4/SpecTec.lean

(This is still on a branch, see <https://github.com/Wasm-DSL/spectec/pull/2> for status on its merge progress.)

Posting this here in case someone wants to play around with it.

And, thinking a bit bigger, maybe some people want to get behind a community effort making the Lean4 formalization of the WebAssembly spec at least as good as the Isabelle one (maintained basically by one very talented person, Conrad Watt) and the Coq one (maintained by a research group around Philippa Gardner).