2 ms·
The linked spec of wasm is written in English. Can we even say it's "formal"? Did anyone specify wasm using something like Coq, Lean or Isabelle/HOL?
by nextaccountic 2y ago
The linked spec of wasm is written in English. Can we even say it's "formal"?
Did anyone specify wasm using something like Coq, Lean or Isabelle/HOL?
- steveklabnik 2y agoI agree that people mis-use the “formal” word when it comes to specifications. But on this specific question, https://www.cl.cam.ac.uk/~caw77/papers/mechanising-and-verifying-the-webassembly-specification.pdf https://www.cl.cam.ac.uk/~caw77/papers/mechanising-and-verif... is the work I am aware of.
- lifthrasiir 2y agoWebAssembly is specified in an English prose and a formal notation, as you can see from, for example, [1]. It is still true that a (mathematically) formal specification can suffer from bugs due to the lack of verification, but it is much easier to verify an already formal specification than a prose specification. It is also possible to turn a prose into a formal specification if the prose in question is already close enough to the formal notation, like ESMeta [2]. [1] https://webassembly.github.io/spec/core/valid/instructions.html https://webassembly.github.io/spec/core/valid/instructions.h... [2] https://github.com/es-meta/esmeta https://github.com/es-meta/esmeta