So uhh...
Today's #projects is the first known to me #webassembly runtime in #lean4 complete for a tiny subset of #wasm.
I'm going to keep going deep before refactoring and supporting the entire bredth of the standard.
When people tell you that #wasm is a simple VM they don't lie. The problem is that it's still a pretty big VM with a lot of features. Implementing it is approximately as easy or as hard as implementing a C99 compiler.
I mean, it's sort of easier, but maybe twice as easy. Not by an order of magnitude.
That's why I strongly suggest the following path for implementers:
1. Read the whole spec and try to understand it. Read some blog posts, play with wasmer like it's shown in some example repositories[1].
2. Implement a #wast parser into Exprs. Ignore #wat.
3. Implement a thing that instantiates and runs Exprs.
After you experimented with your runtime enough, you'll be able to easily extend it with binary capabilities. I made a mistake of supporting emitting binary format before writing the runtime and while it was a nice, fun and necessary experience that allowed me to learn way more about wasm binary encoding, it didn't inform the architecture for the runtime and by the time I started runtime, deadlines were tighter than I'd like them to be, so my architecture is garbage.
But runtime architecture is the most important architectural decision you'll be making while implementing #wasm runtime, so don't repeat my mistakes and work on it first.
After you're happy with all the important bits, write binary serealisation / desearialisation with an assistance of hexdumps of the files you made in (1).
