Hacker News new | ask | show | jobs
by mananaysiempre 505 days ago
You can understand the WASM spec in your sleep if you’ve ever worked through a type-system paper from the last two decades (or a logic paper from even earlier I guess).

Granted, not many people have, but there’s a reason why it makes sense for it to be written in that style: they want it to be very clear that the verification (typechecking, really) algorithm doesn’t have any holes, and for that it’s reasonable to speak the language of the people who prove that type of thing for a living.

The WASM spec is also the ultimate authoritative reference for both programmers and implementers. That’s different from the goals of an ISA manual, which usually only targets programmers and just says “don’t do that” for certain dark corners of the (sole) implementation. (The RISC-V manual is atypical in this respect; still, I challenge you to describe e.g. which PC value the handler will see if the user code traps on a base RV32IMA system.)

1 comments

> You can understand the WASM spec in your sleep if you’ve ever worked through a type-system paper from the last two decades

Is there a lot of crossover between those people and people who work with assemblers or code generation? There's even more crossover with those people and understanding how to read a minimal ISA document.