These are chat archives for jdubray/sam
It's spaghetti in the sense that proposal, mutation and state representation are not clearly delineated
why is it such a problem to not do this
The problem though is when you are working in a larger team and across time (when people leave/join the team or when you are working on the code you wrote 6 months ago), the question innevitably becomes (even when the code is really good), what does this code do?
More examples implemented in AsmL (ASM verification tool): https://asml.codeplex.com/wikipage?title=Examples&referringTitle=Home
Shortly, I think ASM is predecessor of TLA+ / SAM , it describes states, but changes model in place