[erlang-questions] Erlang and Akka

Jesper Louis Andersen jesper.louis.andersen@REDACTED
Mon Sep 1 12:58:53 CEST 2014


On Mon, Sep 1, 2014 at 10:28 AM, Wojtek Narczyński <wojtek@REDACTED>
wrote:

> Type checking is basically automated theorem proving.


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:

* Get the programmer burden down to a manageable level
* Make it expressive so you can describe complicated protocols with ease

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.


-- 
J.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://erlang.org/pipermail/erlang-questions/attachments/20140901/8286742e/attachment.htm>


More information about the erlang-questions mailing list