[erlang-questions] Erlang and Akka
Jesper Louis Andersen
Mon Sep 1 12:58:53 CEST 2014
On Mon, Sep 1, 2014 at 10:28 AM, Wojtek Narczyński <wojtek@REDACTED>
> 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.
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the erlang-questions