It feels so weird to program in languages that compile modules not top-down as #Lean4 does.

On one hand, it's really cool that I can now put the most important functions up top; on the other hand, it defies logic!

I'm surprised that Lean 4 isn't getting more attention. It's a...

• dependently-typed general purpose #functionalprogramming language...
  • with a syntax that instantly feels more familiar than Haskell/Agda/Idris, more readable than ATS, and nicer to write than Coq
  • that supports some amount of interactive development
  • that I think is reference counted? There's a paper called "Counting Immutable Beans" that seems to indicate that it is, but I haven't read it
  • that compiles to native binaries
  • that has its own dedicated build system that uses makefiles written in Lean
  • that interfaces with external C code
  • and still has facilities for theorem proving

Seems like an interesting system for people who want to make use of #dependenttypes. #Lean4

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).

[1]: https://github.com/cognivore/wasm-sandbox

What an evening to parse some #webassembly with #lean4, a dependently-typed language.