Comment by pron | Hacker News Reader

Comment by pron | Hacker News Reader

Parent Full thread

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?

In the TicTacToe spec, we have

    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.

Reply on news.ycombinator.com