[erlang-questions] Looking for tricky protocol examples for verification research

[zxq9]

In other words, you want to define a contractual way that different processes 
can verify the external behavior of one another, instead of doing the actor 
version of duck typing that we tend to use all the time?

If this is a runtime thing (and it would have to be in the case of empty 
processes which get assigned their behavior at runtime), then there would have 
to be a way to interrogate a process and ask it what messages it listens for 
and what the return type (if any) or side effects (if any) of receipt of those 
would be. Actually, it wouldn't be hard to write a framework or behavior that 
did exactly that. You would, as always, be depending on the programmer to not 
forget things and for processes to always tell the truth (consider the games 
we play with Dialyzer).

Is this sort of what you are getting at?

-Craig

On Thursday 30 October 2014 17:43:51 Jonathan Schuster wrote:
> More generally, I'm looking for the kinds of scenarios that one might use
> contracts to specify in a non-concurrent world: instances in which you
> expect some component you're interacting with to have a certain behavior,
> so you specify that behavior in some way that the computer understands. My
> hunch is that something similar could be useful for communication-focused
> programs, but it's unclear what. It would be especially useful if anyone
> points out in these examples "at line X of file Y, I want to state
> invariant Z but have no way of doing so".
> 
> From what I've seen, session types come closest to solving this problem,
> but they tend to be overly restrictive, and it's not obvious how to apply
> session types to actor-based programs, because session types assume that
> channels are created separately from the processes that receive messages on
> them.
> 
> I'm especially interested in examples that expect a particular behavior
> from PIDs sent as messages, since this adds an extra layer of complexity
> not normally addressed in the classic communicating finite state machine
> literature. Session types deal with this with what they call "carried
> types", and I'm curious what other mechanisms I might be able to devise for
> those situations.