This group is about TLA+ and its tools. TLA+ is a language, based on
the logic TLA, for precisely describing algorithms and high-level
system designs. It is unlikely that this group is what you're looking
for. To advise you if it is or where else you should look, I need to
understand what you are looking for.
You wrote that you became interested in concurrency and want to learn
about its concepts and issues. The problem is that "concurrency"
meant something completely different for Robin than it does for me.
To me, the field of concurrency encompasses a body of algorithms and
a few impossibility and complexity results. Perhaps the most important
of the impossibility results is the Fischer, Lynch, and Paterson (FLP)
theorem that is described on the Web as follows:
In a distributed system with asynchronous message delivery, no
algorithm can guarantee to reach a consensus between participating
nodes if one or more of them can fail by stopping
The preeminent conference on this subject has been PODC. I will call
that subject Dijkstra concurrency, since he began it. I will let
Milner concurrency be the subject that Robin meant by the term
concurrency. I believe he originated it with his work on CCS
(Calculus of Concurrent Systems), and I think its preeminent
conference has traditionally been Concur. I believe that only one of
the 82 papers cited in the book by Robin that you mention has had even
the slightest influence on Dijkstra concurrency. (That one is Hoare's
paper on CSP, which inspired a handful of long-forgotten papers in the
80s.)
The relevance of Dijkstra concurrency to practical system building is
obvious, though for quite a few of the algorithms studied it's hard to
see any application yet. I will leave it to others to comment on the
practical relevance of Milner concurrency. The only one I've observed
is that it has inspired specification languages and tools that have
seen some use in industry.
TLA, like Robin's bigraphs, is a formalism. Formalism has played no
significant part in the discovery of any results in Dijkstra
concurrency. (Results in Milner concurrency seem to be mostly about
formalisms.) TLA and I/O Automata have had some influence on how
algorithms are described and proved correct. I've found that TLA has
helped me to think more clearly about what correctness of algorithms
means. But you can't learn Dijkstra concurrency by studying TLA, nor
by studying any of the formalisms from Milner concurrency. I intended
the TLA+ Hyperbook to have a track about some simple principles of
Dijkstra concurrency, and it contains one or two chapters of that
track. However, it's not now a very good introduction to Dijkstra
concurrency, and I don't know if it ever will be.
So, are you interested in Dijkstra concurrency, Milner concurrency, or
something else?
Leslie
Going off on a tangent, but If I were to reduce TLA+ to a (perhaps obscure) buzzphrase, I’d say it is “theory B for (and by) theory A people”. This is felt not only in the choice of the extremely general computational model of abstract state machines as opposed to some more specific algebra (or “calculus”), but also in the emphasis on and interest in how “plain engineers” can (and do) put it to use in practice. I think that this emphasis (and even interest) is sorely lacking in some of the theory B work, which may result in the real-world efficacy of some of its most interesting work remaining forever unknown.
While it is true that TLA+ is completely orthogonal to PL concerns, I do think that there is some real competition here, certainly in the approach (and I’m sorry if I’m stirring a pot which should not be stirred). Even though TLA+ is a formal language, I think — and correct me if I’m wrong — that it is firmly in the verification camp, which basically says “express your program how you like, we’ll give you tools to reason about it”, while the PL camp says, “we’ll give you tools to express programs in a certain way, and if you do, they’ll be easier to reason about”. I guess that the PL people would say that their very approach would inevitably result in fewer of their attempts being adopted (it’s easier to adopt a tool that fits how you already work, than a tool that requires you to change how you work to fit with it), but they hope that those few ideas that eventually do get adopted would have a long lasting, revolutionary impact. In a way, it is a competition between pragmatists and idealists, I think. As a "plain engineer" practitioner, I, for one, would be very interested in seeing a panel discussion between the two different camps.
Ron's post raises two questions. The first is, do we need to specify
programs in a higher-level language before implementing them in a
programming language? People who design PLs would say no, their
languages make what the program does so obvious that no higher-level
description is needed. I think the first PL for which this was
believed to be true was FORTRAN. It's not true for FORTRAN and I don't
think it's true for any existing general-purpose PL--certainly not
when it comes to implementing distributed systems.