<div dir="ltr"><div class="gmail_extra"><br><div class="gmail_quote">On Mon, Sep 1, 2014 at 10:28 AM, Wojtek Narczyński <span dir="ltr"><<a href="mailto:wojtek@power.com.pl" target="_blank">wojtek@power.com.pl</a>></span> wrote:<br>

<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Type checking is basically automated theorem proving.</blockquote></div><br>Yes and no. Trying to infer a type from a term is a search problem, more or less. Checking that a given term has a type is more akin to verifying a proof under a set of rules or policies. The hard part about session types and friends is how you:</div>

<div class="gmail_extra"><br></div><div class="gmail_extra">* Get the programmer burden down to a manageable level</div><div class="gmail_extra">* Make it expressive so you can describe complicated protocols with ease</div>

<div class="gmail_extra"><br></div><div class="gmail_extra">I do think we are ready to take ventures into this, but I would definitely start with a runtime check and then extend it later with a static notion once we know what are the properties we want to eradicate at compile time. Like a normal type system, we will let things slip through - the trick is just to place the abstraction level so we reap the benefits for little cost.<br>

<br clear="all"><div><br></div>-- <br>J.
</div></div>