A big theme in LLM-enabled software dev is that verifiable correctness makes it much easier to take bigger leaps with LLMs. E.g. tests, compilers, state machines, etc. While researching for databuild, I recently came across colored petri nets, and instantly saw opportunity.
Colored petri nets (CPNs) are an extension of petri nets. Petri nets are essentially directed bipartite graphs where places can contain tokens, and places are connected by transitions (where the side effects happen). In petri nets, a single token contains no data, and represents an identity-less tokens location in the net. Importantly, petri nets with transitions that have only one input and output and one token globally are equivalent to finite state machines. Colored petri nets extend this model, allowing individual tokens to have data associated with them. This allows CPNs to match closely to the Rust typestate pattern, and suggests Rust may be able to implement CPN semantics easily.
CPNs are of particular interest because a) it is still hard to write concurrent applications and b) provide the potential for formally verifying concurrent programs at build time. Also, if we can implement a high performance datastore underneath, a CPN framework might be able to handle the hard parts of concurrent applications: state synchronization, conflict detection, deadlock avoidance, and coordinating access to shared resources. These are enabled via two other features of CPNs: guards and multi-token consumption/production.
A guard is a list of boolean conditions that may apply to a transition: things that must be true for a token to take that transition. For instance, there need to be more than 0 connections available in the connection pool to claim one. Multi-token consumption/production is just what it sounds like: a fork in the network via a transition, where P1 -> T1 -> (P2, P3), so T1 consuming a token from P1 produces a token in each of P2 and P3 simultaneously. Conversely, a join in the network via a transition, where (P1, P2) -> T1 -> P3, would require that both P1 and P2 to have tokens present that are able to transition via T1 into P3, which will also be simultaneous.