|
|
|
|
|
by veltas
500 days ago
|
|
> actually quite readable, although some of the language can be a bit intimidating if you're not used to reading programming language papers You're more generous than me, I think it's rubbish. Would have been easier to read if they had written it more like an ISA manual. |
|
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.)