Protocols/Formalism

24 Sep 2025 - 06 Oct 2025

What is Formal Protocol Theory? describes the work of SIGFPT, a group devoted to developing formal techniques for modelling protocols. See the Roam page for the ongoing work.

Mostly the focus has been on "mathy" representations like Petri nets, Communicating Concurrent Processes, with occasional dips into category theory. I'm not a big fan of these, and have been lightly pushing in different directions. I've had a hard time explaining why, so this page attempts to lay out my thinking a bit. I apologize for being carping and critical, and should acknowledge that many other people in the group are grappling with the issues and trying to come up with better solutions.

The FPT group has looked at a bunch of different theories and formalisms, but seems to have neglected the simplest and most obvious way to model a protocol: as a set of communicating procedural objects. That is, let's say you wanted a model of a protocol, say traffic. You could make rule-based agents for the cars, the lights, any other entities involved, and run them in a simulation. This is maybe not as elegant as more declarative mathematical formalisms, but its (a) much easier to construct and understand (b) produces cool animations to spur further thinking and experimentation.

I've suggested some moves in this direction (eg using the more object-oriented Actors model of computation, or one of the existing agent-based modelling frameworks like SugarScape or NetLogo. SugarScape is mentioned as a "lodestar" Woodenman Group 1 but in general there doesn't seem to be a ton of interest in this approach.

The nice thing about agent-based modelling is that a child can understand it (this is the basis for Logo). It's a powerful thinking tool, and much more accessible than more mathy formalisms like CCS or category theory. I've built systems like this in the past, such as Behave! (an animal-behvior modelling environment designed for maximum non-technical accessibility). And see Vivarium Project for a more expansive version of the idea of a learning/simulation environment.

Of course it depends on the goals of formalism. If it is to make iron-clad proofs about tightly-defined technical protocols, then you might want something more mathy. That stuff has its uses, to be sure, eg in cryptocurrency or networking. But most of the interesting stuff in protocol theory deals with vaguer, more human-centric protocols, and those seem less amenable to this kind of thing.

The strongest mark against these formalisms is that they are rather forbidding to people without a math background. The protocol field is trying hard to be inclusive of non-technical people (artists, policy people, activists) and a tool that is too mathy won't be of much use to them.

This is kind of a separate argument and has the problem that it is really against any kind of formalism, not just the mathy ones.

One of the canonical examples used in the SIGFPT is handshaking. I haven't actually seen a formal model for this but you can imagine what it looks like: one party sees another, approaches, extends hands, grip, release, while the other party acts accordingly. You can make a state diagram for this, but it will probably fail to capture what is interesting about handshaking, all the subtle social cues involved in it. Here eg is a paper that tries to get at that with a Erving Goffman -microsociology lens: The handshake as interaction by Hall & Hall.

A 'good' handshake, according to Vanderbilt, is 'elbow level, firm, and brief' (1972:241). Post says, The proper handshake 'is made briefly, but there should be a feeling of strength and warmth in the clasp' (1940:23). Bad handshakes include the bone crusher — the grip that makes the other person, especially a woman wearing rings, wince. Or a limp, damp handshake that seems to say, 'I am not really happy to meet you at all!' Or it may be the kind of straightarm shake that seems to hold the other person off or the octopus grip that draws you inexorably toward the shaker, who never seems to want to let go.

Another key aspect of protocols that tends to be left out of formalizations is enforcement and violations. Protocols are not mere patterns of action, but social objects that people orient to, make use of in structuring their behavior, and violate when they can get away with it. This is the point of Ethnomethodology, roughly that the formal structures of protocols are not constitutive but are the product of people's improvised social activity. This is also their most interesting aspect.

None of this is really an argument against formalism, just that I find the interesting bits of protocols lie in the areas where formalisms are weak.

Instead of mathy formalisms (or in addition), focus on agent-based modelling. Build an environment and modelling language that looks like rule-based Actors or something, where protocols can be expressed in simple condition-action rules. Make it easy for people to run simulations involving a lot of interacting agents, and vary parameters, do experiments. NetLogo is an existing platform that could be used for this. Run workshops where people are trained to build models, put them up in public.

Perhaps this is just a different effort than formal theory. Call it protocol modelling or simulation or somesuch.

Why not procedural modelling?