@swetland @mcc yeah, I also found the spec difficult to navigate (to make it worse it has some obnoxiously resource-hungry javascript that renders formulas)
my understanding is that the spec is written with one main consumer in mind: people doing formal verification of the spec. the secondary consumer is people with a lot of PL experience writing runtimes. everyone else isn't really considered, in practice if not in theory