If you create a query language, then the state can be verified to match expectations at any point.
I'm not sure why we don't program like this.
I don’t really know what you’re talking about, and have a hard time imagining how ideas from relational algebra can be applied to all APIs.
For example, many database-like things already use relational algebra and an actual query language, for sure. But how does this apply to, say, a GUI toolkit or an audio device driver?
it may be that a bug only shows when hundreds of transitions are performed (like an overflow or bug due to large data), but that's more stress testing. many bugs have repros involving a few state transitions.
relational algebra is a useful tool in my opinion because much of programming involves adding/removing things from sets or testing for their membership in a set. also relations are powerful as they can express recursive ideas like which widgets are contained within others (from the GUI example).
relations also allow defining invariants at a high level which must be true at any state. (eg, there should be no state like: audio_buffer_is_empty and audio_playing)
additionally we have languages such as SQL or for example https://alloytools.org/applications.html that can help programmers specify this in a familiar way.
Is it necessary to be able to exhaustively enumerate states? I remember a project I worked on some years ago which had me sketching out a statechart for a system which was not structured as an explicit FSM. The end result was surprisingly complex. I imagine some systems might even have an unbounded number of “states.”
I’ll definitely read more about Alloy too.