[mjb]

Other languages to add to this list would be Dijkstra's Guarded Command Language, and Promela. Promela is especially interesting because of the (nondeterministic) execution semantics, which provide an extremely interesting way to model parallelism. In a similar vein, TLA+ is worth a look.

Both Promela (Spin) and TLA+ have active communities and have found fairly wide use in industry. They are generally used for model checking, model extraction by guided abstraction, and development by refinement, but can be used in a much more adhoc way to just experiment with parallel ideas.