A logic is a formal language with syntax, derivation rules, and a definition of validity. Message Logic is an example logic.
An operationalization is a description of how something is computed. This might be in code (most direct), but a specification that describes data structures and how to compute things (e.g. the RM specs) also qualifies.
Models
At the moment, I think we have three basic computational models which serve different purposes:
The engine model, developed primarily by @jonathan and @graphomath, and specified most recently in this ART report, models independent processes which keep state, track timers, send messages, and may create new processes. This is the “lowest level” model in the sense that it aims to correspond closely to the actual physical computational system and that we aim to build everything else (operationally) as engines.
The resource model, currently implied (but not formalized) by the RM specs, and gestured at somewhat in this topic, models “resources”, the atomic units of state in our distributed system. All applications which we want to run on top of this distributed system must ultimately be compiled to this logic.
The object model, roughly implied (but not formalized) by @mariari’s investigations, aims to be a higher-level representation including a first-order “object” concept which would be ergonomic for developers to program in.
@Jamie has also been working on an “Idealized Anoma” logic which – as I understand – aims to be a “logical compilation target” for all three of these specific logics (but we have yet to determine exactly what that means, since these logics are themselves not yet fully defined).
Open Questions
How does the engine model (logic) relate to the object model (logic)?
How can we incorporate information flow control in the object model (which I would argue we must), and what does the compilation look like here (non-trivial)?
Per discussion with @tg-x we should add a “layer” to the engine model which incorporates pub/sub (need to figure out some distinctions around content-based / topic-based).
It’s important to note the distinction between language and model – a model is a logical essence, with syntax and derivation rules, but generally the absolute minimum featureset required to model accurately whatever aspects we are aiming to model, where a language has many decisions about features and syntax which are not related to (or at least not fully determined by) what is being modeled. In this sense, for example, “Anoma-level” is really a model, not a language.
In general, we need different (specific) models for (a) local vs distributed machine, (b) different data consistency levels (e.g. totally ordered vs eventually consistent), (c) different primary entities (e.g. immutable resource vs mutable object vs engine instance), (d) IFC vs non-IFC (details TBD, but what metadata we track or do not track), … (possibly more)
Resource machine logic: this is a distributed one, and should cover where computation is happening. A derivation corresponds to a sequence of transaction (function) creation, solving, composition, and ultimately transaction function execution and verification steps, where in a sense the last check is a check of the validity of the derivation (all for a single transaction). This should be sketched out in more detail.
Indexing / views of the distributed state - should this be a logic at some point? How is this related?
IFC may correspond somehow to steps in the derivation (which must be done atomically, so one party/location must atomically do each step), where a ZKP could in principle be made at each step. This is fuzzy but worth thinking about more.
I recommend reading pages 10 and below, this talks about the paradigm shift we underwent that made us start talking about languages instead of systems.
“A system is a set of interacting components, though sometimes the interaction is in the realm of ideas—and thus a language can also be a system. But the usual case requires a set of actual, observable behavior. A real set of things doing real stuff. —Even if in a computer.”
