| > I imagine that they mean something like this (which is also almost valid prolog, and mozart/oz, and some others) Kind of, but notice that I mentioned receive statements. Those are important. I'll show what I mean this time, because I guess people aren't picturing what I'm describing: https://gist.github.com/tsutsu/5543bcaec4448b1de0023fbde31c8... (Got way too long to fit in an HN comment.) > they start to act like something adjacent to types Not just "adjacent"; automata are monoids! I think I saw a language reify this concept once — where you were able to declare an abstract state-machine interface/protocol, and then the compiler would check that for implementations of that interface/protocol, each function actually has the proper precondition states (i.e. only reachable from those states' functions) and postcondition states (i.e. has live code-paths reaching exactly those functions.) Interestingly, I think it did this with individual types for each state-transition function, rather than there being a single higher-level type for the digraph of functions. Anyone know what language (or maybe it was a computational proof assistant) I'm referring to? |