A simple actor definition

Building correct software requires a clear specification of what the system must do and an implementation that shows how to do it [1]. The Actor Model provides a powerful abstraction for concurrent and distributed systems by treating computation as asynchronous message-passing between independent entities.

• Provide a clean, minimal definition of an actor
• Illustrate it with a stopwatch example
• Describe a practical method for defining new actor types

• Writing by progressive refinements
• Type Theory
• Laws for communicating parallel processes [2]
• Actor model of computation: Scalable robust information systems [3]

In order to simplify notations, we introduce α#msg(param …) to mean "send the message <:msg, param …> to the actor α". In other words:

α#msg(param …) :≡ send(<α, <:msg, param …>>)

In our definition, receive is presented as a blocking operation that halts the actor’s execution until a message arrives. It is a practical concession rather than a theoretically pure one.

In the strict Actor Model, actors are entirely reactive. They do not contain an explicit "blocking loop" that pulls messages from a queue; rather, the runtime pushes messages to the actor, invoking its current behavior. The actor reacts, designates its next behavior via become, and goes dormant.

However, building complex control flows solely with reactive state transitions can be ergonomically challenging. Consequently, mature industrial implementations — such as Erlang and Akka — blend the Actor Model with sequential processing.

They provide an explicit, blocking receive construct that pulls messages from a mailbox. Our definition adopts this pragmatic approach, acknowledging that the ability to write sequential, suspendable code is critical for the usability of an actor system in practice.

A protocol may be defined using a specialized language called Session Types [4], [5]. For instance, given:

health :≡ GET /health: !{ "health": "ok" } . end
hello  :≡ GET /hello: !"world" . end
server :≡ &{ health, hello }

then the protocol server has branch named health. The branch health may be interpreted as: "If I receive the HTTP request GET /health from a client, then I should answer with a JSON string that maps to { "health": "ok" } which terminates the protocol." The associated coprotocol is:

health :≡ GET /health: ?{ "health": "ok" } . end
hello  :≡ GET /hello: ?"world" . end
client :≡ ⊕{ health, hello }

Note that there is a deviation compared to the official notation. For instance, we let the reader translate ?{ "health": "ok" } to "I expect to receive a string that can be mapped to the JSON value { "health": "ok" }".

The example shows how to define a stopwatch and the different steps that hold for all actor subtypes definitions.

How to define some kind of actors?

In practice, note that the proof is usually approximated by tests.

The following helpers provide a convenient way to create and use stopwatches:

Stopwatch$mk : Oscillator → Stopwatch :≡
  osc ↦ spawn(script(osc) 0)

Stopwatch$read : Stopwatch → ℕ :≡
  sw ↦
    sw#read(self())
    receive
      <sw, seconds> ↦ seconds

Client invocation (an actor itself) example:

sw1 :≡ Stopwatch$mk(osc)
sw2 :≡ Stopwatch$mk(osc)
t1  :≡ Stopwatch$read(sw1)
t2  :≡ Stopwatch$read(sw2)
print("t1: #{t1} seconds")
print("t2: #{t2} seconds")

A smart compiler or runtime may execute independent parts in parallel:

∥
  - sw1 :≡ Stopwatch$mk(osc)
    t1  :≡ Stopwatch$read(sw1)
    print("t1: #{t1}")

  - sw2 :≡ Stopwatch$mk(osc)
    t2  :≡ Stopwatch$read(sw2)
    print("t2: #{t2}")

The Stopwatch$read function works with any actor that satisfies the stopwatch protocol. This highlights that interfaces in actor systems are defined by protocols rather than concrete types. This enables greater flexibility and composition.

New actor types can be introduced using the following template:

* <Name>
:PROPERTIES:
:TYPE: 0672475a-1dfa-4aa0-93d5-add1c1c995ad
:ID: <UUID>
:END:

<Informal: what does it represent? Why is it needed?>

** Protocol

<Description of accepted messages and responses.>

** mk : 🞎 ⇢ Name

<Constructor description.>

** <msg> : Name Args ⇢ Reply

<Message interface description.>

We use dashed arrows ⇢ to indicate that replies are not guaranteed, the recipient may crash or be struck by lightning, instead of plain arrows → that would have had indicated functions.

We have provided:

• a minimal yet usable definition of actors
• a clear separation between protocol and implementation
• a concrete stopwatch example with proof
• a practical three-step workflow for constructing new actor types

This definition of the Actor Model achieves its primary goals: it is minimal, pedagogical, and maintains a clear separation between protocol (specification) and implementation. The inductive proof technique shown with the stopwatch example provides a practical way to reason about correctness.

However, the stopwatch actor halts immediately upon receiving any unexpected message. While this choice simplifies the model and the proof, it is overly rigid for practical applications. Real-world actor systems typically employ supervision, logging, or graceful degradation rather than unconditional termination on unknown messages.

Additional limitations include:

• Absence of timeouts on receive, which can lead to deadlocks in more complex scenarios.
• Lack of structured error handling and supervision hierarchies.
• The proof technique presented only addresses sequential message processing and does not yet cover fairness, message reordering, or network partitions.
• The core primitives remain low-level; many applications would benefit from higher-level patterns built on top of them.

These observations open clear paths for future refinements of the model.

We have presented a minimal definition of actors based on five core primitives: send, receive, become, spawn, and ■. By putting protocols first and supporting them with concrete implementations and proofs, this article offers both a practical methodology and a foundation for building understandable concurrent systems.

The stopwatch example demonstrates that even with very few primitives, one can construct useful, provably correct behaviors. This protocol-centric approach naturally leads to flexible, composable, and evolvable designs.

This work is a first approximation in the spirit of progressive refinement. Future versions may incorporate session types, supervision primitives, timeouts, and tighter integration with type theory.

Actors can learn and negotiate protocols dynamically. This property allows actor systems to evolve into complex, adaptive “living systems” [6], [7], [8], [9].

A protocol may be viewed as a challenge — i.e., a request for the server to "prove that" it can behave according to a certain specification. If the server cannot satisfy the protocol on its own, the client may teach it the required definitions, algorithms, or sub-protocols and help it construct the proof. In effect, the parties negotiate how the server should prove the required property. The client may also decompose the original proposition into smaller sub-propositions and negotiate only those that the server is able to prove. The whole process of reaching such an agreement is what protocol negotiation really means.

Finding a way to make computers perform this kind of sophisticated negotiation automatically (for instance by combining session types with AI and interactive theorem provers such as Lean) would be a fascinating research direction.