[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: Robin Milner Space and Motion of Communicating Agents

Thanks for such comprehensive responses.

I have started reading the TLA HyperBook. Thanks for making such a clear text available. 
When I have read that I'll be able to respond more clearly.

My interest is more in understanding systems than concurrency on its own. 
I work in a business day to day, and struggle to explain the simplicity and complexity of the business to each person within it.

I started my reading with Jay Forrester's papers on System Dynamics. 
I then read John Sterman's Business Dynamics.
However, Sterman ends by suggesting that agent based modelling is a new and important way of understanding Systems.
I also consider Chris Argyris as very important in systems thinking.
All of them emphasise the importance of making mental models explicit, and testable against past data.
I completely agree with what I have read so far in the TLA HyperText book on the importance of specifications.

Milner made me wonder whether there is a new way of understanding communicating agents, but as I have said I find his work very hard to understand.

I will continue to look for ways to find a tutor or course I can take which helps me understand.

In response to your points above about the intersection of programming languages and specifications, I agree that the first purpose of writing a program is for humans to read and secondly for computers to execute. (SICP https://mitpress.mit.edu/sicp/front/node3.html)

One of the books on my list to complete is The Haskell Road to Logic, Maths and Programming. 

The Haskell Road to Logic, Maths and Programming

I found the notion of types very interesting, and the use of Haskell to check types to be important.
I take your point that a Haskell program may not be very easy to read.

I just want to find a more firm foundation for understanding systems and communicating agents.

thanks again,


On Friday, May 13, 2016 at 11:07:26 AM UTC+1, Leslie Lamport wrote:

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.

It would be nice if there were a PL that made higher-level specs
unnecessary.  I think many people working on Milner concurrency have
that as their goal.  I believe it would be possible to compile TLA+
specs that use a specific way of describing interprocess communication
into adequate code for a useful class of distributed programming
problems.  Testing that belief would be an interesting research
project.  I believe that if specs separate from programs are ever made
completely unnecessary, it will not be by PL development.  Rather, it
will come through advances in machine learning that allow code to be
generated from something that looks more like a TLA+ spec than like a
program in any currently envisioned language.  But that is pure
speculation, and should not be taken seriously.

The current need for specs as well as programs raises the second
question: should those specs look as much as possible like programs to
make them easier for computer engineers to write?  I think most
engineers would answer yes.  I say no.  I think the most important
function of writing a spec is to make the engineer think clearly about
what she is building.  I have found conventional programming languages
to be impediments to clear thinking.  TLA formalizes the way I learned
over many years to think about concurrent algorithms--the heart of
Dijkstra concurrency.  I developed TLA+ to be a language that forces
engineers to think that way about their concurrent systems, rather
than the way PLs lead them to think.

I have given my answers to these two questions, but I don't have time
to justify them properly.  I would be interested in knowing how
engineers who have used TLA+ in building distributed systems answer
them, and why.