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