My claim is not false: state machines do not "require" linear types, but that is not what I said. I said linear types are what you want if you want to encode th

My claim is not false: state machines do not "require" linear types, but that is not what I said. I said linear types are what you want if you want to encode these things in a natural way. Substructural (linear) types are ALL ABOUT encoding stateful propositions in the type system. Even if you had an expressive dependent type system, the best way to type check a stateful protocol would be to add substructural types to it! See http://users.eecs.northwestern.edu/~jesse/pubs/dissertation/tov-dissertation-screen.pdf http://users.eecs.northwestern.edu/~jesse/pubs/dissertation/... for a good discussion of encoding stateful propositions with substructural (linear) type systems.