[derefr]

I feel like we don’t need a novel language for this. There’s already a pretty-well-known language that’s almost a DSL for “making complex finite-state machines easy to create”: Erlang.

I know that sounds wacky, so let me pitch you on that idea :)

In ‘primitive’ Erlang (i.e. Erlang without OTP), each FSM state is just a function, that can contain its own event loop (`receive` statement) to accept input, and then can transition to a new state based on that input by tail-calling another function.

Such an Erlang module is a direct, 1:1 encoding of the FSM you’d draw on paper — and very readable as such — but is also plain-old executable Erlang code! In fact, this is basically the most idiomatic Erlang code you can write, syntactically. It’s when the language is at its best and most compact/expressive. (It’s also when all of Erlang’s weird syntax choices suddenly make perfect sense.)

You can easily author+maintain an FSM with a large/complex tree of states and sub-states, by just putting each state function with its various sub-state functions into its own module, and then having each module only expose the valid entry states for each sub-state set.

Because each independent FSM exists in its own actor (virtual thread of execution), you don’t need any more than this. You don’t need to worry about the data representation of the FSM — the FSM’s data representation is the actor’s process record + stack. And you don’t need to worry about how to “pump” the FSMs; they’re pumped by the runtime scheduler. (However, if you care about pinning down your concurrency model — e.g. if you’re trying to model a DSP — there are Erlang libraries for specific abstractions like CSP channels that you can use to do so.)

It’s very easy to write a static analysis pass to verify that a primitive Erlang module like this constitutes an FSM “and no more” — i.e. that it could be transpiled into any other formalism that instantiates an FSM (e.g. a regex; a DSP; etc.) Erlang even breaks down its compiler into helpful separate reusable components (all available to any Erlang program) to help you do this. And these components make it just as easy to do the actual transpilation, turning this Erlang code into whatever other kind of encoded formalism you like.

But, unlike most such formalism DSLs, it’s very easy to also break out of the FSM abstraction, and trade it for a more powerful one, if an FSM no longer works for your use-case. You’re working with regular Erlang code. So, if you just do a regular stack-frame-pushing call instead of a tail-call, now your FSM is a pushdown automaton. Or, if you pass a state variable on the stack along with each tail-call, now you’ve got a Turing machine.

Honestly, ignoring all the stuff about concurrency, Erlang source code / BEAM bytecode is an almost perfect abstract machine for reifying various computational formalisms in an externally-verifiable way. If I was working on a computational proof for some CS conjecture, I’d heavily consider 1. writing the problem statement in (primitive, non-OTP) Erlang, and then 2. writing a small transpiler that would convert Erlang to lemmas in Z3 or Coq. (I’ve already done this once or twice, actually.)

And, if I were implementing something like Cloudflare’s Edge Workers “but for FSMs” (e.g. some user-submitted pattern-matching automata for structured data, to filter user subscriptions to that structured data) then it’d be an extremely easy decision to standardize on (a restricted, static-analyzed at submit-time sub-ISA of) BEAM bytecode as the user-submitted program format. I would then just implement my worker server as a regular Erlang server that would load+run those checked BEAM modules.

[JohnHaugeland]

> I feel like we don’t need a novel language for this.

Well, there's like 50 others, many of whom are in heavy use in industry, so, I guess I feel like a lot of people think this is useful.

.

> I feel like Erlang is already a great language — almost a DSL — for “making complex finite-state machines easy to create.”

Erlang is almost my favorite language.

I've tried using both of its finite state machine libraries. I do not find them to be usable. The results are extremely verbose, and if one goes over around 30 states, I cease to be able to debug them.

The natural implementation of the TCP/IP state machine in FSL is eight lines; 315 bytes. The TCP/IP Erlang state machine example floating around is like ten times that size.

I find debugging that thing exhausting.

.

> It’s very easy to write a static analysis pass to verify that a primitive Erlang module like this constitutes an FSM “and no more”

It's not clear to me why you would want this

.

> Honestly, ignoring all the stuff about concurrency, Erlang source code / BEAM bytecode is an almost perfect abstract machine for reifying various computational formalisms

It can't implement anything without Okasaki juggling. You and I are in strong disagreement here.

FSMs are a great example. You either need to reach outside the Beam VM with `hipe_bifs:array` or you need to copy the entire machine state every time you want to mutate it.

.

> And, if I were implementing something like Cloudflare’s Edge Workers “but for FSMs”, it’d be an extremely easy decision to standardize on (a restricted, static-analyzed at submit-time sub-ISA of) BEAM bytecode.

At Cloudflare's scale, the inability to implement mutably would become a serious performance problem.

[derefr]

> I've tried using both of its finite state machine libraries.

I'm not talking about gen_fsm or gen_statem — note how I said "without OTP" above. I'm talking about writing Erlang the way it was originally conceived before proc_lib existed — where each process has a module that's exclusively responsible for its own receive loop, rather than being a delegate module for a generic receive-loop manager framework (proc_lib).

That kind of Erlang code produces simple, easy-to-analyze bytecode. It doesn't integrate well with supervisors or whatever, but interoperation with the rest of the Erlang/OTP ecosystem isn't the point. You don't call into arbitrary slap-dash non-formalized libraries within code that's supposed to represent a mathematical formalism. (E.g. you wouldn't call an arbitrary library from within a PEG grammar DSL. This is why e.g. Yecc's Erlang callbacks happen after parsing, rather than instead of parsing. If they happened instead of parsing, you'd break the formalism of the parser, and wouldn't be able to trust that your grammar does in practice what it was proven to do in theory any more.)

Instead, you create your own little world inside the formalism, that maybe imports a few reusable pre-proven abstractions compatible with the formalism, or that opaquely maps into pre-proven abstractions that exist within the prover (e.g. Z3's bit-vectors.) Abstractions are available in most-any other interpreter / prover / generator / whatever-er for the same formalism.

> FSMs are a great example. You either need to reach outside the Beam VM with `hipe_bifs:array` or you need to copy the entire machine state every time you want to mutate it.

Why are you mutating something outside the FSM from within the FSM? If the only state isn't "the state" (i.e. what box you're in on the FSM diagram), then what you have is not an FSM (in the computability-theory sense) any more.

The point of an FSM is to reduce the "power" of reasoning needed to prove things about the abstract machine — and so to be able to make guarantees that Turing machines cannot make, like being able to prove termination — by constraining what side-effects an operation within the abstract machine can have. An FSM can only switch its state among one of a usefully-enumerable number of options, e.g. the set of functions in a module, or the possible values of a single machine-register. A pushdown automaton can only switch its state among the sets of all possible sequences of such usefully-enumerable options (i.e. stacks of FSM states.) Etc.

(Note that Erlang/OTP's gen_fsm and gen_statem aren't FSMs in the computability-theory sense, since they pass along a state variable. They can be used as such if you don't put anything in that variable — or even if you put a scalar in that variable and constrain its size — but even if you don't use it, the resulting bytecode still passes that variable along in a way that makes it harder to translate the bytecode into prover lemmas. But all the remote-call stuff to proc_lib code that's not part of the proof already makes that nigh-on impossible, so....)

I think we might be talking about very different things here but both calling them "FSMs." I'm talking about how Erlang's native syntax is really good at expressing https://en.wikipedia.org/wiki/Deterministic_finite_automaton (like non-backtracking regexps) succinctly. What are you talking about?

[JohnHaugeland]

> note how I said "without OTP" above

I apologize for overlooking this

.

> You don't call into arbitrary slap-dash non-formalized libraries

Respectfully, no, it sounds like you write them yourself, instead

.

> > FSMs are a great example. You either need to reach outside the Beam VM with `hipe_bifs:array` or you need to copy the entire machine state every time you want to mutate it. > > Why are you mutating something outside the FSM from within the FSM?

I'm not. I'm talking about the expense of the action of the FSM mutating itself.

.

> The point of an FSM is to reduce the "power" of reasoning needed to prove things about the abstract machine

I apologize, but you and I have strongly contrasting opinions here.

The rest of you trying to teach me what an FSM does is noted. Thank you for your time

.

> I think we might be talking about very different things here but both calling them "FSMs." I'm talking about how Erlang's native syntax is really good at expressing https://en.wikipedia.org/wiki/Deterministic_finite_automaton (like non-backtracking regexps) succinctly. What are you talking about?

My library, and finite state machines, which are the superfamily containing DFA and a great many other things. DFA is not a common interpretation of the phrase FSM; usually that phrase means a Mealy machine or a Moore machine, or maybe a Harel machine.

I think you're spending more time attempting to force this library to implement some computer science term you're familiar with than is warranted. JSSM doesn't fit any of those labels well.

DFAs are generally a small group of functions meant for parsing strings. JSSM isn't even superficially similar to a DFA, and most state machines in practice aren't implemented that way in my personal experience.

[derefr]

> Respectfully, no, it sounds like you write them yourself, instead

I write them myself and prove them, and then use them.

Or, more likely, I take code from elsewhere, reduce it to its core, prove that — if possible; it often isn't, because code from elsewhere is often fundamentally Turing-hard — and then, if I was able to prove it, use it.

Or, even more likely, I use a library of self-contained code that lives inside the prover's model, that someone else already did all the hard work of getting the prover to accept.

Think of it like this: would you call an arbitrary utility function from an HTTP library inside a reference implementation of a cryptographic cipher?

No, because that arbitrary utility function has no abstract-mathematical equivalent. You can't prove anything about code that contains a black-box like that. The code, with the call to the HTTP library inside it, isn't a discrete-mathematics-specified-in-procedural-language proof of anything any more.

If you want to prove anything about code, the code needs to 1. live inside your proof (along with all its transitive dependencies), and 2. be modified such that all its base types are types that have complete models in your chosen prover's algebra (e.g. no non-fixed-size bit-vectors.)

> I apologize, but you and I have strongly contrasting opinions here.

What are FSMs "for" in your mind, then?

I use them when I want to be able to prove the behavior of something formally, and then reuse the proof as a production-quality implementation of that thing as-is. This allows the design↔implementation equivalent of "documentation drift" to be avoided — you don't have to trust that the programmer that translated the math into code did it correctly this time; you just have to trust a single compiler/code generator (that itself can have been proof-verified.)

I use FSMs for the same reason I use PEGs, or cellular automata, or other such formalisms, in place of just trying to prove an abstract Turing machine: because there are known ways to prove certain properties of these low-power formalisms in bounded time, while there's no known (or sometimes, no possible) equivalent for Turing machines generally.

> My library, and finite state machines, which are the superfamily containing DFA and a great many other things. DFA is not a common interpretation of the phrase FSM; usually that phrase means a Mealy machine or a Moore machine, or maybe a Harel machine.

You're being a lot more pedantic here than I was attempting to be. I meant to refer to "deterministic finite-state transducers" — the class of thing to which Mealy machines are a subset. But people on HN don't know what those are, while they do generally know what a DFA is. And a DFA has the same computational power as a Mealy machine generally; it's just a special construction of one (like a Binary Search Tree is just a special construction of a Binary Tree.)

I was trying to contrast with NFAs, which aren't FSMs (deterministic finite-state transducers) at all, but rather are computationally-equivalent to pushdown automata.

Maybe, rather than a DFA, I should have made the analogy to LR parsing, which also has equivalent abstract-computational-power requirements.

[faeyanpiraat]

I do not know anything about erlang, but I’m intrigued about your proposal.

Could you make a github repo with an example project implementing your solution?

[odipar]

I was very much in favour of (abstract) state machines, especially the Rebel DSL that was developed in Rascal.

A very nice thing about Rebel is that it can do (bounded) model checking using SMT solvers.

Currently, I believe (Pure) Objects (with restrictions!) are a better approach because it doesn't require a paradigm switch. We already know them and they are also little state machines, right?

If done right, we can also do explicit model checking etc, version control.

Actors/Erlang/Akka is also a good choice, although they add some complexity compared to objects: it's hard to do synchronous calls with Actors for instance.

[JohnHaugeland]

There are two FSM implementations in the standard library. Just use those.

[JohnHaugeland]

Pattern matched state machines are how Prolog, one of Erlang's parent languages, is expected to work. This is how they implement horn clauses.

I can't speak for parent poster, but, I imagine that they mean something like this (which is also almost valid prolog, and mozart/oz, and some others:)

  -module(pattern_match_tl_fsm).
  -export([ next/1, disable/1, enable/1, enabled/1, may_pass/1, create/0 ]).
  
  next(red)    -> green;
  next(green)  -> yellow;   % allow the lack of a match to throw for off; there is 
  next(yellow) -> red.      % no next state for a light that's turned off
  
  enable(off) -> red.       % allow the lack of a match to throw for every color;
                            % only lights turned off may be turned on
  disable(red)    -> off;
  disable(green)  -> off;   % allow the lack of a match to throw for off; cannot 
  disable(yellow) -> off.   % disable if already disabled
  
  enabled(off) -> false;
  enabled(_)   -> true.
  
  may_pass(green)  -> true;
  may_pass(yellow) -> careful;
  may_pass(red)    -> false;
  may_pass(off)    -> careful.
  
  create() -> off.

And then you can do stuff like

  TrafficLight = pattern_match_tl_fsm:create(),
  TurnedOn     = pattern_match_tl_fsm:enable(TrafficLight),
  Step2        = pattern_match_tl_fsm:next(TurnedOn),
  etc

For very simple things this is probably a great choice, and OP is correct to suggest that this is very debuggable, especially if those states are tagged tuples instead of lazy-example atoms. However, the rate at which it doesn't scale is magnificent. By contrast:

  import { sm } from 'jssm';
  
  const make_light = () => 
    sm`off -> red => green => yellow => red; [red yellow green] ~> off;`,
  
  const safety     = { red: false, green: true, yellow: 'careful', off: 'careful' },
        enabled    = light => light.state() !== 'off',
        may_pass   = light => safety[light.state()];
  
  export { make_light, enabled, may_pass };

And that gives you basically the same interface for way less code.

Of course, bringing in an interpreter and/or a compiler isn't zero cost, so if you only have a couple of the straight module ones, the first notation honestly can be a pretty good approach, and given Erlang's module compositional nature, it's frequent to have things that in other languages would be unrealistically simple. By example, the TCP/IP state machine is 11 states and 19 edges, and in my opinion would make sense in the first notation as its own standalone module in erlang. I believe that parent post has a solid point.

The reason one tool hasn't universally won is that there isn't a best way to do this, style of thing. Trade-offs.

Still, with the sm`` notation, I find that I very frequently one-liner state machines with <= 6 states, and that in my head they start to act like something adjacent to types. Like ... behavioral enumerations? Things that simple which behave in a fixed fashion are sorta-types in my head, and they become very easy to use as a structural element. I dunno. They start getting low-ish level-ish to me, especially when they're behind generators, even though in reality that isn't true at all. The library is sufficiently fast and sufficiently tested that I feel comfortable using them that way, at least.

Also, when you start thinking about larger state machines, which sometimes have 50 states and 200 transitions, it is my opinion that that they grow at such different rates can quickly become important. When I say the TCP machine with 11 and 19 makes sense as a standalone, to me, that's getting not too far from the upper limit of where I'd think spelling it out manually was smart. (Still, to be fair, most FSMs are simple, rather than complex, so that's not all that harsh of a cutting criterion in the balance.) Even when hyper-dense, my opinion is that the sm`` arrow notation can easily carry 10x the structure on-screen and be comfortably readable than the typical datastructure based approach.

For me, the `jssm` chain is modifying how I think about code in some subtle ways, and that makes me feel like there might be actual value there. I hope you'll give it a shot and tell me whether or not you agree.

HTH

[derefr]

> 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?

[odipar]

I agree with you. Especially breaking out of the abstraction when needed. I believe Akka also has a FSM abstraction on top of Actors.

[JohnHaugeland]

Transpiling to Z3 and Coq is an absolutely fascinating idea.

I will attempt to adopt this. I've no idea where even to start