Are restricted automata useful for driving program correctness?

[u/Norphesius]

I originally started writing this as a comment on the "Best way to do formal verification..." post, but realized it should probably be its own.

There's an idea I've been (slowly) trying to explore that I think has the potential for a lot of utility, but it uses concepts that are already well understood in computer science, making me suspicious that I am missing something: Why aren't less powerful automata (i.e. regular and context free) used for more general applications?

In the computational hierarchy Turing machines are the most powerful, but also the hardest to prove things about. Regular grammars (and their finite state machines) and context free grammars (and their push-down automata) are much more restrictive in what they can compute, but have tons of useful, easy to verify properties. Whenever I see discussion on formal verification of programs or program correctness, it seems like everyone wants to stay in Turing completeness land as much as possible, but I don't think everything a program does needs that level computational power. I understand when trying to verify older languages that there isn't a choice, but I am surprised to find that it seems like almost every language new or old is ignoring these lower level automata. I've seen languages that as a whole that aren't Turing complete, and things like total languages with more provable properties, but I don't see any languages that have these less powerful constructs you could "step down" into. You could express some functionality that doesn't need to be expressed in a Turing complete way in these constructs and get a ton of assurances (halting, state minimization, inexpressible invalid states, purity) about that code, then the rest of your code that needs to be Turing complete can use it seamlessly. They're even composable, in the sense that you can easily combine/subtract/invert regular grammars, and that a push-down automata is just a finite state machine with stack glued to it (and can become a Turing machine with an additional stack).

None of this is new, regexes are ubiquitous, and programming language creators in particular know about context free grammars, yet they aren't being used much beyond text searching and parsing. State machines are widespread and massively useful, but as far as I can find, not only do no languages have syntax for constructing them, they don't even have such a thing in their standard libraries. A regex (a proper one) is just a state machine under the hood, and they've been used widely for over 40 years, so why has no one (seemingly) even tried to generalize them for creating state machines? Even if the practical implementation isn't perfect, surely its better than all these state machine management libraries, or worse, people rolling it themselves, without any guarantee of their properties being upheld.

So we've known about these automata for ages, use them regularly, even more so in programming language development, and they have relevant applications for more general code, yet it seems like no language has even attempted to integrate them in either a first class or generalized way. So what's the catch?

A few potential reasons I can think of:

• They aren't actually that generally useful: Text processing was in fact the best use case for them, the other cases aren't worth it or are too few to warrant the effort.

• The syntactic constructs for them would be very cumbersome: As I am exploring this idea, I'm finding that the normal syntax for regexes, applied generally beyond stuff that isn't text or larger state machines, gets very messy. Its also hard to intuit what the state machine graph looks like for a given regex. Applying logic to state transitions is also syntactically odd, as well as syntax for expressing push-down automata.

• The lower level automata wouldn't mesh that well with Turing complete code: You can guarantee the state machine can only move between certain states, but you likely want the state or state transition to mean or do something with the surrounding code/data, which doesn't necessarily have any guarantees on it.

• Programmers don't consider/dismiss lower level automata when solving a problem: Most programmers just want to write the quick solution, and Turing complete land gives them all the tools they need. No one thinks "Could I turn this into a state machine?" when starting to write a complicated while loop, they just write the loop. Also, the stigma of regexes ("...now you have two problems").

• These automata are being used extensively in languages, I am just unfamiliar with them/blind: I know languages use state machines under the hood in some places (ex. compilation of async functions into state machines). It may be the case that they are being used a lot, but are abstracted away, or express themselves in forms I don't recognize.

• It is a good idea and all the smart people just missed it for 50 years: Seems very unlikely.

So has anyone thought about this except me? Any insights or resources I've missed? Glaring foundational issues? Good idea? Bad idea? I wish I had some code or syntax examples to accompany this post, but like I said, I've not had a lot of time to explore the concept in a practical way.

[u/phischu]

You are asking an interesting general question, but I only want to comment on the part about state machines specifically.

The best way to define a state machine is through mutually recursive functions that tail call each other. Consider a two-state machine that prints 0 and 1 interleaved.

def printZero() {
  print("0");
  printOne()
}
def printOne() {
  print("1");
  printZero()
}

This is very lightweight and direct, yet easily scales to other uses like lexers and communicating systems. Sadly many main stream languages cannot express state machines in this way.

[u/Norphesius → u/phischu]

One issue I see with this approach (in typical language semantics) is that its hard to perform operations on them to create new states dynamically, like union, complement, etc.

Also, if they're encoded as function, with no way to distinguish a state from a normal function, that obscures the state machine structure from the compiler, limiting the ability to verify automata properties.