I can't believe finally someone mentions behavioral programming here on HN. I'm a huge proponent of it and have written some in the context of React https://lmatteis.github.io/react-behavioral/
How does it compare with TLA+ though? I've tried reading through your document, but I can't seem to understand how the interweaving is done and the blocking.
Behavioral programming is built on top of a paradigm called synchronous programming, developed by David Harel (who later invented behavioral programming), Amir Pnueli and later Gérard Berry and others. The mathematical formalism underlying synchronous programming (in the same way that the lambda calculus underlies functional programming) is temporal logic, introduced into computer science by Pnueli (for which he received the Turing Award). TLA+ is based on a logic called TLA, the Temporal Logic of Actions, which Lamport designed to fix what he saw as some shortcomings in Pnueli's approach. So there's the connection.
Harel and Pnueli wanted a formalism that makes it easy for both humans and machines (formal verification) to understand. Formal verification with model checking is, of course, also central in behavioral programming. I guess you could say that synchronous programming (and so behavioral programming, which is a kind of SP) is related to TLA+ in a similar way to how Haskell is related to, say, Agda.
Interesting I see. I thought BP was built on top of Live Sequence Charts - a visual formalism for describing specs that can also be executed.
Thanks for the info. I'll have to dive a bit more into TLA+. Even though I still don't see how the request/wait/block is implemented in TLA+... I mean you still need an even selection mechanism for it or not?
Next2 ==
/\ turn' = turn + 1 \* A
/\ current' = Opponent \* B
/\ ∃i,j∈1..N: \* C
/\board[i,j] = Empty \* C.1
/\ board'[i,j] = current \* C.2
For `Next2` to be true, the square [i, j] has to be empty AND in the following state, that same square must have whichever mark was `current` in it. Since `current` switches between the two each step of the behavior, this forces each player to wait until their turn comes around.
> I thought BP was built on top of Live Sequence Charts
Yes, but LSC are also based on temporal logic, as were Harel's Statecharts (perhaps the first synchronous programming language).
> I mean you still need an even selection mechanism for it or not?
Not sure what you mean by "even." TLA+ is nondeterministic, and the formulas can serve as rules to restrict that nondeterminism (where simple logical conjunction is used to compose the rules). Also, nothing is really "implemented" in TLA+, as it's not a programming language. It's a formal specification language that describes the behavior of discrete systems.
I'm pretty sure the (here much maligned) Eve programming language was an example of this. It was posted a few times before its demise. I'm also a fan of the paradigm, particularly Eve's relational/behavioral style.
Not quite behavioral (which is a very specific thing), but Eve was certainly synchronous. It was one of the two languages (the other being Céu) that brought synchronous programming from the niche of safety-critical realtime systems to more mainstream software. IMO, it was the most theoretically-advanced programming language around.
How does it compare with TLA+ though? I've tried reading through your document, but I can't seem to understand how the interweaving is done and the blocking.