These are all better, depending on the audience. What are the chances of generating (or in some way automatically aligning with) something like the ordinary math of the Yellow Paper from a K specification? The math itself is no big deal: ‘and’, ‘or’, ‘not’, ‘there exists’, ‘for all’, ‘if and only iff’, ‘is an element of’ … It’s the presentation of the math that hurts, and the presentation could easily be much better. And as bad as it is I can follow the Yellow Paper’s description of the EVM much more easily than I can KEVM. (And yes, that’s because I’m too lazy to learn much K until I really have to, whereas I’ve been dealing with bad math notation for over five decades
That is, I want the power of K, but I don’t want to give up the familiarity of ordinary math to myself and most any other engineer or scientist.
Failing that, I’d go for a syntax closer to either Python or Solidity, as those are languages most used by the community for describing algorithms and interfaces.