You might like "System design from provably correct constructs", it's written by James Martin but it's presenting the work of Margaret Hamilton. She developed

You might like "System design from provably correct constructs", it's written by James Martin but it's presenting the work of Margaret Hamilton. She developed the ideas while working on Apollo 11 https://archive.org/details/systemdesignfrom00mart https://archive.org/details/systemdesignfrom00mart In modern terms it works by allowing the user to edit a kind of abstract syntax tree (without the syntax) using only operations that preserve correctness (essentially type checking) so you literally can't make a bug. (You can still make a program that does the wrong thing correctly.) The four essential operators are (of course) sequence, branch, loop, and parallel (non-interference). (As you note, state machines are useful for describing complicated systems, but they themselves are simple in terms of the four operations.)