Over the past month or so I have been working on a pull request to webassemblyjs1. With quite some effort, many failing test cases and lots of help by Sven who maintains the project, we recently managed to merge it. For me this has been pretty much the most interesting (and challenging) programming I have done so far. To summarize the pull request in a few bullet points:
- Opened the pull request on April 3rd, merged on May 14th.
- 75 commits
- 1400 lines of code (including tests)
I have already written an article about the type system itself2 which describes in detail what it means to type-check a WebAssembly module. This post contains more meta notes about the kind of programming involved in a type checker.
There are (at least) two kinds of thinking about code correctness. Whenever I encountered a case where my logic failed there were two ways to proceed
Let’s fix this case!
Why is this wrong?
Throughout the whole thing I found myself moving from the first kind to the second kind. The first mode of thinking focuses on specific examples and typically the code ends up reflecting that by catching more or less exactly that case. While this gives more green test cases in the short run, this strategy can only work for code with a small number of logical paths. Given that a type checker should work on any valid3 input program, the number of logical paths is mind numbing.
In the second mode of thinking which I call spec thinking, all examples are created equal. Instead of thinking about how my code will type-check a certain example, I started focusing on how closely my code reflects the specification.
Test coverage and requirements
One of the most frustrating things in programming is changing requirements. The great thing about implementing a type checker for a language with a formal specification is that it is all there. The validation section of the WebAssembly specification can answer any question that might come up during implementation. There even is an official test suite4 with a huge amount of test cases, so whenever I am unsure about how something works I can just copy in a relevant test case. I realized that programming against a detailed specification with good test coverage makes a huge difference in how fast I get frustrated.
I never really thought about designing the format of an AST (abstract syntax tree) before and always assumed it as given. However, a lot of code in the type checker directly reflects the AST format and I started thinking about alternative representations. It turns out that there is a lot of freedom in designing the details of an AST format and doing this well to make code simple is difficult. We are now regularly updating our format and converging to a good design I believe.
Actually it should even work on invalid input programs because you want nice error messages when type errors occur. This is really difficult. ↩