Sequential functions can be used to define and compose large scale state machines that represent computer software and hardware. The mathematical basis is introduced and there are motivating examples, including a proof of the safety of the Paxos algorithm. https://www.yodaiken.com/wp-content/uploads/2023/12/fac_sm_published_acm.pdf
