> 2. typing of acceptable messages - that's way harder, as you need to model state in the typesystem - imagine "does this variable represent an open or closed f

> 2. typing of acceptable messages - that's way harder, as you need to model state in the typesystem - imagine "does this variable represent an open or closed file handle" and then updating that as the code calls `open`, `read` and `close` appropriately... I think that would be a good use case for Dependent Types.