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).

[(deleted)]

Hello I'm resurrecting this thread

[(deleted)]

WebAssembly has changed so much and it has so much potential

[(deleted)]

It is a widely used programming language with a rigorous specification, so it's very useful in program verification

[(deleted)]

Do you think it's wise to build a program verification framework based on WebAssembly

[(deleted)]

Despite "assembly" in its name it's closer to a high level programming language than assembly code

[Julia Scheaffer]

I am certainly interested. One of my back burner projects is a compiler targeting WASM, and I am interested in writing some of the software with lean. Having a formal specification of WASM in lean would be very useful.

[Julia Scheaffer]

I currently have a prototype compiler written in rust, but I'd like to transition to Lean so that I can use stronger type theory :smile:

[Julia Scheaffer]

I think that writing a verified WASM interpreter in Lean would also be a fun project (I don't know if Lean is particularily well suited to do this)