The Rust language (by Mozilla) is putting statically verifiable state machines in the type system: http://lambda-the-ultimate.org/node/4009 http://lambda-the-u

The Rust language (by Mozilla) is putting statically verifiable state machines in the type system: http://lambda-the-ultimate.org/node/4009 http://lambda-the-ultimate.org/node/4009 It's based on Typestate, a really good 1986 paper: http://www.cs.cmu.edu/~aldrich/papers/classic/tse12-typestate.pdf http://www.cs.cmu.edu/~aldrich/papers/classic/tse12-typestat... I hope this idea catches on in other programming languages.