[erlang-questions] Why single-assignment with non-shared state?

Ulf Wiger <>
Sun Oct 21 12:30:40 CEST 2007

2007/10/21, Matej Kosik <>:
> Hm. Today I have look at the Wikipedia article and it (at the begining) says:
> "The sequential subset of Erlang is a functional language".
> This is correct.
> However, Joe's new book says:
> "Erlang is a functional programming language and has nonmutable state."
> (page 32, at the top)
> Isn't this false? With `spawn', `send' and `receive' you can model mutable state---the state of
> processes changes over time and this is very useful. The change of the state can be observed from
> the outside. Isn't this contradictory to the reality?

Within each process, state is nonmutable. Observing from the outside,
it appears as if the state of a process is changing, and processes can
communicate with each other through messages; they cannot alter the
state of another process (short of killing it).

If you take a broader view of 'state', to include also the contents of
the mailbox, then it is possible to alter the state of another process. (:

> I agree that fragments of code written in Erlang's functional subset can be subject to
> proof-techniques (about program correctness) developed for functional programs but what about the
> non-functional constructs? Have you developed some proof techniques to cover also these constructs?
> Which? I am interested. (I do not mean crashes).

Within limits, erlang code can be converted to uCrl, which can then be used
for model checking. There is another approach that post-processes trace
output from a running system, abstracting away detail from the trace, and
then e.g. model checking the abstract trace. There are some other approaches
as well.

Ulf W

More information about the erlang-questions mailing list