[TYPES] Types in distributed systems

[Peter Sewell]

> The TL;DR version is: how does one specify types in a distributed
> programming model, like actors? And how much can we trust these types?

As you can see from the earlier responses, there's been a lot of work
addressing different aspects of this problem.   To quickly (and
partially!) summarise, we have:

- typing to ensure message-passing endpoints conform to some protocols
(session types etc.), as several people have mentioned

- partially typed systems, in which type-checking part of the system
ensures that its interactions with some other untrusted (and hence not
necessarily type-correct) part will not be disastrous.   Andrew
mentioned James Riely and Matthew Hennessy's work on this, Jan Vitek
and I dabbled in this direction
(http://www.cl.cam.ac.uk/~pes20/wrapall.ps), and there's a lot of more
recent work, especially in non-distributed PL contexts (eg Richards et
al.'s OOPSLA 13 paper, like types, etc.).

- typing that ensures safety properties in the face of version change
of some of the endpoints.   Phil mentioned our Acute language, and
there's also the HashCaml follow-up
(http://www.cl.cam.ac.uk/~pes20/hashcaml/index.html).   These explore
how one can preserve type abstraction boundaries using only runtime
checking of channel-name identity - basically implicitly versioned
communication channels.

- typing to ensure that dynamic updates of endpoints will work, as
explored by Mike Hicks and others.

Peter