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
Skip to PDF contentState machines for large scale computer software and systems