bubble sort now (deactivated) (May 01 2023 at 15:29): bubble sort now (deactivated) (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
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: https://link.springer.com/chapter/10.1007/978-3-030-90870-6_4 - one way to discover more is to look at 1. citations in that paper and 2. who has cited that paper, e.g., https://cs.au.dk/~birke/papers/iris-wasm.pdf
Paolo Giarrusso (May 01 2023 at 16:11):Since you ask about notation, what about http://siek.blogspot.com/2012/07/crash-course-on-notation-in-programming.html ?
Last updated: Apr 20 2024 at 01:41 UTC