I’m not sure If you are really convinced that’s true or it’s supposed to be understood as an exaggeration. It is subjective, and I’ll grant it’s not the most i

I’m not sure If you are really convinced that’s true or it’s supposed to be understood as an exaggeration. It is subjective, and I’ll grant it’s not the most intuitive thing to look at, but I don’t agree it’s worse than assembly. Besides the readability of the specification is not some priori limitation. Sel4 spec example definition set_endpoint :: "endpoint ⇒ data ⇒ state ⇒ state where set_endpoint ep data s ≡ s (ep := (IdleEP, data))