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

[Jonathan Schuster]

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?


> 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).
>

Again, I'm thinking of something closer to types or contracts where we
don't assume the programmer always specifies the right behavior: any
"wrong" behavior by the program would (ideally) be detected and reported.

Really, though, I'm not sure exactly what kind of solution I'm targeting
yet. I've observed that it's generally difficult to do the kind of
reasoning I'd like to do in languages like Erlang, and I'm currently
looking for concrete examples of this kind of problem. Then the plan is to
study those examples, try to find a common pattern, and figure out what a
useful solution would be. Without concrete examples, it's difficult to know
if I'm solving the right problem.

Regarding Dialyzer, I haven't actually used it myself, although I've read
about it. Can you tell me more about what kinds of games you have to play
with it?
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://erlang.org/pipermail/erlang-questions/attachments/20141031/4b64d86c/attachment.htm>