Archived in favour of https://github.com/Wasm-DSL/spectec.
This project provides a domain-specific language (DSL) for describing WebAssembly (or Wasm) specification. This can then be used as the single canonical representation, from which one can automatically derive:
- human-readable specification,
- a reference interpreter,
- stubs for proof assistants, and more.
The DSL is written as a library in OCaml.
The Wasm specification is light years ahead of specifications for other languages when it comes to clarity, unambiguity and size. Even so, it can be improved:
- Currently, each validation and execution rule is written twice, once in prose and once as a mathematical judgement. This can lead to inconsistency and provides an additional burden on writers of the specification.
- The mathematical judgements are written in LaTeX, which is not everyone's cup of tea.
- The specification is not machine readable (unless one wants to parse prose or LaTeX) and cannot be used in further analysis.
The problem is becoming more and annoying with the growth of the specification.
The easiest way to test the project is using dune. Once installed, you can rune make, which will result in a main.exe executable. Running it will produce a human-readable output of the currently implemented specification.
Why not use an existing tool like Ott?
The reason is twofold. First, none of the existing tools support the exact outputs we want to achieve without significant rewrite. Second, the structure of the Wasm specification (syntactic families, typing and reduction rules, …) are well established, and putting them in a general tool discards a significant amount of domain-specific knowledge.
The main reason is to not introduce yet another standard. Furthermore, defining a new language requires a parser, a runtime, and so on. The additional flexibility that an independent DSL brings is relatively small if one uses a reasonably flexible host language.
OCaml is a reasonably flexible host language. Furthermore, it is well established in the WebAssembly community, being the language in which the reference interpreter is written.
Have you considered writing your DSL in tagless-final style?
Yes, the first prototype included a tagless-final variant. It turned out to be longer than the usual tagged representation, was more confusing for newcomers, and made it harder to perform manipulations (which is the main goal of the project).