<html>
<head>
<meta content="text/html; charset=utf-8" http-equiv="Content-Type">
</head>
<body bgcolor="#FFFFFF" text="#000000">
On Sat, Aug 30, 2014 at 5:42 PM, Wojtek Narczyński <span dir="ltr"><<a
moz-do-not-send="true" href="mailto:wojtek@power.com.pl"
target="_blank">wojtek@power.com.pl</a>></span> wrote:<br>
<blockquote
cite="mid:CAO0g3iFt3YSFe=kqMvA9oRGTpjRq0R_0fi_LEeF8Sj9dQR-xeg@mail.gmail.com"
type="cite">
<div dir="ltr">
<div class="gmail_extra">
<div class="gmail_quote">
<blockquote class="gmail_quote" style="margin:0 0 0
.8ex;border-left:1px #ccc solid;padding-left:1ex">
<div> It is extremely difficult to verify protocol
adherence statically. <br>
</div>
</blockquote>
<div><br>
</div>
<div>What do you mean by "difficult"? Lacking tooling
support? Requiring too much heavy work on manual
annotations? Or something else...<br>
</div>
</div>
</div>
</div>
</blockquote>
<br>
Probably all of this and more.<br>
<br>
It is even difficult do design a correct protocol, for example SIP
has deadlocks built-in. CHORD also had it's problems.<br>
<br>
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.<br>
<br>
As for the tools, there are quite a few, but they are external to
the programming languages, so they check models, not
implementations.<br>
<br>
If you are interested in this (fascinating) subject, this is a good
place to start reading:<br>
<a class="moz-txt-link-freetext" href="http://www.cs.princeton.edu/courses/archive/spring10/cos598D/FormalMethodsNetworkingOutline.html">http://www.cs.princeton.edu/courses/archive/spring10/cos598D/FormalMethodsNetworkingOutline.html</a><br>
<br>
-- <br>
Wojtek<br>
</body>
</html>