This original talk / blog post was one of the major reasons that I started playing around with Isabelle. I had taken a look at Coq and the Software Foundation series a few months earlier, and it just couldn’t click with me. As you see in this post, modeling systems in Isabelle doesn’t feel like “math” at all, and feels very much like programming in an ML-family language.

I actually get a huge benefit out of modeling things in Isabelle from this alone! Proving things is great, but being able to formally specify something is the really important skill. I seriously think people would benefit from just writing models and proof skeletons like this, without even finishing proofs. Learning different proof techniques comes with time, not that I’m even an expert on that yet.

For example, in the post, an entire distributed system is simply modeled as:

datatype ('proc, 'msg, 'val) event
  = Receive (msg_sender: 'proc) (recv_msg: 'msg)
  | Request 'val
  | Timeout

type_synonym ('proc, 'state, 'msg, 'val) step_func =
  ‹'proc ⇒ 'state ⇒ ('proc, 'msg, 'val) event ⇒
  ('state × ('proc × 'msg) set)›

Taking away some of the polymorphic type noise of the step_func declaration, it becomes:

step_func =
  ‹'proc ⇒ 'state ⇒ event ⇒
  ('state × ('proc × 'msg) set)›

A step_func is just a function that takes a process ID, current state, and an event as input, and returns a new state plus a set of messages to send to recipient processes. This is enough to model any distributed system! That’s not that complicated at all.

You may also be thinking, hey - that looks like the Elm Architecture or Redux. And you’d be right - TEA is literally just a functional design pattern of a state machine, and again, this simple definition is enough to reason about all of computation.

Anyway. Great post, great tool, happy to see Larry and Martin collaborating, and I always love a good state machine model of a system.