Re: [Caml-list] Re: Where's my non-classical shared memory concurrency technology?

[Martin Berger <M.Berger@doc.ic.ac.uk>]

David Teller wrote:

> IIRC, there are already type systems which may prevent deadlocks in
> pi-calculus.

This is true but (1) these typing systems are quite complicated
and it will take heroic educational efforts to push such
new typing systems into programming mainstream; (2) these typing
systems (or at least most of them, the Kobayashi/Igarashi scheme
is extremely general) are  relatively restrictive and many useful
concurrent programming idioms turn out to be not typable.

Regarding (1), I think using such typing systems for concurrency
is completely unavoidable for a variety of reasons, and they will
be adopted in the medium term (in about 10 years), but they are
not ready for the mainstream yet. As to (2), extending the typing
systems is an active research area, and these problems will be
solved eventually. Moreover, recent success in extending Hoare
Logics to concurrency mean that we don't have to rely on typing
systems alone, instead with can take typing systems of medium
complexity to prevent the great majority of concurrency bugs
and have logics for rare hard cases. (Well, that's the hope
anyway!)

Martin