Stream: Coq users

Topic: WebAssembly

view this post on Zulip Huỳnh Trần Khanh (May 01 2023 at 15:29):

hello. I gotta formalize running programs, and I do not wish to use program extraction for a variety of reasons. well I kept saying this in the Lean community and I made a small prototype formalizing a tiny imperative language which transpiles to C++, but it's tiny and disappointing. now I'm a Coq user, and I want to tackle WebAssembly instead. WebAssembly, while being a complex specification, is minimal enough for my purposes. at least less complex than something like JavaScript. and I am aware of the wasm reference manual, which I refer to whenever I need to write WebAssembly code.

the thing is the actual specification is more usable if I want to actually formalize its semantics. I'm aware of WasmCert and it's definitely a good reference. I want to learn how I can get started actually reading the specification to internalize its ideas. I've found its formal notation intimidating but the prose notation is too imprecise for my liking. if you can teach me how I can read the specification, I'd be really grateful.

disclaimer: this is not an academic project. as a college student I'm willing to undertake ridiculous endeavors in the name of thrill and excitement

view this post on Zulip Karl Palmskog (May 01 2023 at 15:59):

WASM is getting formalized in ITPs by everyone and their brother, seemingly in strange and incompatible ways. For example: (one way to discover more is to look at who has cited that paper)

view this post on Zulip Paolo Giarrusso (May 01 2023 at 16:11):

Since you ask about notation, what about ?

Last updated: Oct 04 2023 at 19:01 UTC