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 d

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.