taking for granted the effectiveness of the cryptographic protocol
I agree that taking as an assumption the proper functioning of the underlying cryptographic protocol is an important thing to call out. I would argue that it is strictly necessary in order to properly decouple two hard problems, one which is fundamentally combinatorial in nature (the consensus protocol) and one which is best modeled as continuous, the flow of funds and/or the evolution of other dynamic variables such prices, interest rates, bonding curves, revenue sharing allocations, etc.
I think the scab I am picking at is inverse to the frustration you express: inasmuch as you describe “accounts,” what does that mean for “rights” in terms of “methods,” and similar heuristics.
The methods that I construct are in fact totally chain agnostic (as you note) as they only represent the notion of an operation on the state for which the resulting change in state caused by the operation is explicitly (or implicitly) dependent on both an input provided by the actor and the current state of the system. This is actually so completely generic structurally that there will be examples from any field where there is an pre-specification of a future right to act*, including legal financial where terms and conditions of an agreement include observations or estimation of facts at the time some right is exercised.
The particular definitions in IV are actually just overview of the kind of mathematical constructs one can use to show invariance or convergence (or divergence) in the space of possible states of the system rather than to make arguments about any particular realization. By staying in the realm of possible as implied the structure of a state depend outcome, we get more general tools for informing the design and verification of “contracts” which are primarily defined by the right to take an action which has a predefined outcome as function of the action itself and the state of the system at the moment that action is actually computed on chain. In generally, imagine applying these tools to the set of methods exposed publicly but there is not reason that access control of these methods wouldn’t play a part in applying them to a specific use case.
I see a lot of cases where actions or states in one system would modify the right to access other functions, but for the purpose of proofs in the manner I hope to see, one would not worry about who has access so much as how any use of the methods at anytime but any actor would impact the set of all possible states the system may take thereafter.
I view this work as far from complete both in language choice (because this is a normative process) as well is in the mathematics (which i don’t consider normative). I think the most direct response to concerns about terminology choice would be step up from any terms with use case specific baggage and stay in the realm of formal operators and then only to adapt domain specific language when applying the tools to a particular application. I could happily do without the word account – from perspective we’re talking about spaces, partitions of those spaces, measures of those spaces and functions that may have implications on those measures.
I admittedly struggle to make this to of work accessible to the broader community responsible for implementing programatic contracts for which this concepts serve as important building blocks for rationality agnostic guarantees. Even for engineers trained in fields that rely on such arguments the derivations and fundamentally topological arguments are often out of reach. I’ve studied mathematical models (and design and deployed algorithms) of estimation, decision making and coordination for well over a decade (since ~2003) so I may have had unreasonable expectations of this community regarding the formal study emergent and/or convergence properties of systems.
In fact my aim forward is to see more algorithms with state dependent structures implemented which respect invariants and then to collect actual data from the ethereum network to validate those claims. My R&D firm has its own custom ethereum data collection infrastructure and we’re working on some prototype state-feedback algorithm designs on private test nets.
@phillip, Thanks for the feedback. I hope this helped answer some of your questions.
*I would argue that the physical world it self has this property. We have naturally the right or ability to take physical actions (like exert forces on things to move them) that don’t violate the law’s of Newtonian physics. To tie it back to your comment about the assumption that the consensus protocol does its job. I view this as being akin to focusing on Newtonian physics for engineering purposes when we know well that these a just scale and context appropriate mathematical models.