Hacker News new | ask | show | jobs
by darioush 467 days ago
If you specify the operations (API) of your system in a relational algebra, then you can use that algebra to generate valid state transitions. (this essentially can construct the tree of continuations the article is discussing or enumerate the paths of this tree)

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.

2 comments

I would love to learn more about this too.

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?

the core idea is to model the state and valid state transitions formally (which may be more directly applicable to the audio driver), so they can be enumerated exhaustively up to a certain bound.

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.

That is fascinating. Thank you!

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.

Do you have a doc or article that describes more about this? I’ve worked with relational algebra before but I’ve never heard it described with an API before. Are the responses all table based? I suppose you could wrap all calls with a SQL style API?