Jello Paper as Canonical EVM Spec

Reasons the YP isn’t a Magician’s Ring yet:

  • We can’t assume by default that YP or other important artifacts of Ethereum belong to any group
  • AFAICT, Yellow Paper editors aren’t organized enough to be called operating
  • The YP is not an EIP, although it should be accumulating EIPs

I predict that YP, JP, and “protocol tests” will be loosely maintained by a single group, each sub-project being somewhat independent, and that this single group will eventually become a Ring :slight_smile:

2 Likes

The Yellow Paper predates the Magicians by years. It didn’t get updated well for quite a while because of copyright hassles. Those are settled, more people are working on it–with Nick Savers in the lead–and it’s keeping up with the EIPs better. I’d say they are as organized as most anything else around here :wink:

1 Like

@grosu
On notation, I think you know that getting rid of the pseudo-XML would remove about 90% of my distaste for the syntax. And a complete K spec of Ethereum would be incredibly useful regardless of the fate of the Yellow Paper. Funding is another matter, and you are not the only team lacking it.

1 Like

Yes. I’m not disagreeing. I just want to stop talking and continue doing. There is no need to talk about one vs the other. People can just do the work.

2 Likes

Exactly my sentiment :slight_smile: People will vote with their time and code.

I’ll continue to help maintain KEVM, people are welcome to contribute PRs.

With KIELE already existing, and KWASM around the corner, I think having a common spec language will yield increasing returns, in the sense that once you learn K once you can read all the specs that are developed in K.

2 Likes

Having a nicer presentation has been discussed many times, funding and/or devs would help turn discussions into action :wink:

<die> xml </die>
:wink:
Believe me, we are all looking for money for K. Sort of a love/hate relationship for me, but at my age I’m used to those.
@grosu @ehildenb @expede @boris

2 Likes

In case the bubble notation above is too colorful, then here is another style for displaying/presenting K semantics, using a more mathematical notation. See, for example, Denis Bogdanas’ thesis on the Java semantics, specifically the Appendix: https://fmse.info.uaic.ro/publication/a-complete-semantics-of-java/. For example, here is a snapshot:


It is really easy to implement such variations; all it takes is to implement the K Latex macros differently in k.sty.

1 Like

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 :wink:

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.

Sorry… what are TMR and n/m?

Correct me if I’m wrong @grosu (you’re more of an expert on K), but it’s totally possible to generate any arbitrary notation, but there needs to be such a generator backend. I’m not sure if one exist for the YP’s notation as of yet, but we could always write one :muscle:

TMR is “triple modular redundancy” (AKA the chronometer example from The Mythical Man Month)

n/m (read “en of em”) is the generalization of the above. TMR is 2/3, but you can have other ratios depending on the tolerances in your system (ex. 7/9)

Ah yes. Yet another TLA :wink: