I’m thrilled to hear that as I’m a big fan of your work!

Thank you for the suggestion as well. Do you have thoughts on specific places where I should either split a chapter and/or associated project to make the ramp up more incremental?

Hm. So the easiest, short term thing might be more annotations. For example, is `on_start` and `on_msg` Rust-isms, or are they particular to this project? If the latter, I'd suggest putting a comment describing what they do in the code itself, and then a separate page describing how they work (with a small, easily modifiable example). Things like that would go a long way to getting people to the expertise-level. Past that, I get the impression there are three ideas here:

1. Actor systems; writing code with Stateright

2. Model checking; model checking with Stateright

3. The actual problems we want to apply Stateright too

Right now you're teaching all three of those simultaneously; I think it would be better if you could scaffold, or introduce the ideas one at a time. For example, showcasing setup and modelchecking first on a property simpler than linearizability. I've been really fond of race-free critical sections for concurrent properties recently, just because it has relatively fewer moving parts.

Sorry these thoughts are a little disjointed, writing guides is really really hard

EDIT: probably not something that would be directly helpful to people, but one thing I'd personally be very interested in reading is how this all works under the hood. If I understanding correctly, you're making each Actor inspectable by `ActorModel`, which then acts as an orchestrator and records history. Is that correct?

Thanks for these insights! I think retaining the actor example while postponing the content on model checking and linearizability might be the way to go. More details on related Rust concepts could be helpful too, given that this may be the first encounter w/ the language for many readers. With that in mind, I’m inclined to break the first chapter into 3:

1. A high level overview of distributed systems and the actor model. Perhaps no code. 2. A Rust intro via an implementation of the Actor trait (which is where the `on_msg`/etc methods can be explained). The chapter would include the same Actor implementation but would omit verification. 3. An intro to system properties, nondeterminism, and verification via model checking. Here the book could postpone a discussion of linearizability and instead indicate a simpler property for the actor system. Linearizability could then be introduced when discussing replication later in the book.

I can also add a supplementary chapter explaining how it works under the hood. You’re correct about `ActorModel`: its a reusable model of actor system semantics parameterized by an `Actor` implementation. Its “dual” is the `spawn` function that lets you run that same `Actor` implementation on a real network.