[erlang-questions] Erlang and Akka

[Wojtek Narczyński]

On Sat, Aug 30, 2014 at 5:42 PM, Wojtek Narczyński <wojtek@REDACTED 
<mailto:wojtek@REDACTED>> wrote:
>
>     It is extremely difficult to verify protocol adherence statically.
>
>
> What do you mean by "difficult"? Lacking tooling support? Requiring 
> too much heavy work on manual annotations? Or something else...

Probably all of this and more.

It is even difficult do design a correct protocol, for example SIP has 
deadlocks built-in. CHORD also had it's problems.

Type checking is basically automated theorem proving. With usual types 
the theorems you write are relatively ease to prove. With protocol 
adherence you'd have to write hard theorems, that might even not be 
provable automatically.

As for the tools, there are quite a few, but they are external to the 
programming languages, so they check models, not implementations.

If you are interested in this (fascinating) subject, this is a good 
place to start reading:
http://www.cs.princeton.edu/courses/archive/spring10/cos598D/FormalMethodsNetworkingOutline.html

-- 
Wojtek
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://erlang.org/pipermail/erlang-questions/attachments/20140901/6f2fe833/attachment.htm>