Yeah, the low quality and informal "tutorial" presentation of the RISC-V "specification" has always been very jarring to me given the popularity of RISC-V.
The authoritative description should be machine readable, but the PDF also needs to be authoritative. That means the PDF needs to be generated from the machine readable spec automatically.
I think the highest quality ISA spec in the industry at this point is ARM's ARMv8/9 ISA manual - it's a readable PDF with psuedocode in a well defined language. Every ISA rule is even given a unique identifier. But even better, it's all generated from XML source files which ARM releases, so you can parse the psuedocode out of those and run that code directly if you write an interpreter for it.
I was hoping to see ARM also release this XML for ARMv8-M but last I checked they haven't done so, sadly.
It's highly worthwhile to examine different ISA manuals to compare their relative approaches (e.g. Power, SPARC, ARMv8, Hexagon, s390x, Itanium, etc.). But I think ARMv8 is the best.
The authoritative description should be machine readable, but the PDF also needs to be authoritative. That means the PDF needs to be generated from the machine readable spec automatically.
I think the highest quality ISA spec in the industry at this point is ARM's ARMv8/9 ISA manual - it's a readable PDF with psuedocode in a well defined language. Every ISA rule is even given a unique identifier. But even better, it's all generated from XML source files which ARM releases, so you can parse the psuedocode out of those and run that code directly if you write an interpreter for it.
I was hoping to see ARM also release this XML for ARMv8-M but last I checked they haven't done so, sadly.
It's highly worthwhile to examine different ISA manuals to compare their relative approaches (e.g. Power, SPARC, ARMv8, Hexagon, s390x, Itanium, etc.). But I think ARMv8 is the best.