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

[zxq9]

On 2014年10月31日 金曜日 11:14:15 you wrote:
> On Fri, Oct 31, 2014 at 12:47 AM, zxq9 <zxq9@REDACTED> wrote:
> > 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?
> 
> It wouldn't be so much the processes verifying each other, but some
> overarching part of the runtime, or perhaps an analysis tool that verifies
> the "contract" for each process. Think of a type system: the type checker
> verifies that every function has the right type, and then a programmer who
> uses the function can be confident that the result of the function will be
> what they expect. I'm not saying I want to invent a type system, but I want
> to enable a similar style of reasoning for concurrent programs, where a
> programmer can just assume that another process acts in a certain way
> because that behavior is checked by another mechanism. Contracts in Racket (
> http://docs.racket-lang.org/guide/contracts.html) also enable this kind of
> reasoning, although with enforcement happening at run-time.
> 
> I'm not sure what you mean by the "actor version" of duck typing, though.
> Could you expand on that, or point me towards an example?

In a duck typed language like Python we can treat anything as some type if it 
implements the basic methods expected of that type. An outside process doesn't 
need to care (sure we could introspect, but needing to is usually regarded as 
a sign of using the wrong tool).

Erlang processes can be thought of the same way if we accept that in Erlang 
"process" means something much closer to what languages like Python mean by 
"object" than is commonly imagined. If I have a game character process it 
might have an AI controller, or it might have a player controller. The 
character process doesn't need to know or care, and we could actively swap out 
AI for player control on the fly and the character process wouldn't care, so 
long as all controllers, regardless of subtype (if we decide to use this term 
"type"), adhere to the "controller" protocol.

Erlang lacks inheritance, so this talk of types is often limited to mean "a 
particular sort of Erlang term()", but in some sense protocol definitions are 
interface definitions that parallel duck typing very closely. This is true of 
any network API as well, actually, hence the loose coupling enjoyed by network 
components that communicate via bland protocols (as opposed to overly rich 
ones nobody bothers to implement).

I think the main issue here is that most protocols internal to Erlang programs 
are informally specified, if at all. The closest thing I see to a contract 
system governing message protocols is Erlang behavior definitions. Come to 
think of it, Erlang behavior definitions might be a good place look for 
inspiration with regard to a message protocol contract system. They mandate 
callback function definitions, but those callback functions are required to 
adhere to certain protocol expectations which are handled directly 
(received/emitted) by functions defined in the governing module of the 
behavior.

These modules could be seen as describing (but not defining on their own) a 
message protocol that could be enforced by contract. Properly -spec'd 
functions would contain the information needed in most cases, but there are 
probably some weird edges there. The only ones necessary to evaluate would be 
the ones mandated by the behavior module (in practice that is mostly true, but 
this is not explicit -- it is not necessary that everything demanded by a 
behavior be ultimately message related).

Blah. I wrote this thinking through it as I typed, so there's almost certainly 
something ridiculous up there. But basically it should be possible to extend 
behaviors or add something very similar to them that would do what you want. 
The problem is that the compiler will care but not the runtime, and this is a 
very different problem.

-Craig