

Hi,
1. Are there existing TLA+ specifications [1] for Erlang?
Recent discussions regarding the behavior of messages for local and
remote processes, the behavior of data in ETS, and the discussion about
a new minierlang all make me think there would be great benefit in
formal specifications of Erlang behaviors.
For instance, I've been thinking about writing various widgets for
distributed applications, each with a well defined TLA+ specification,
and then starting to compose larger and more interesting applications
from them.
My workflow would look like this:
Write widget spec > impl widget > Write application spec (composed of
previously spec'd widgets) > impl application > profit!
The runtime behaviors such as message passing, process linking, etc.
would be the first level that would need specifications... so has this
ever been tackled?
2. Regarding the minierlang, I'd really like to get involved in this
project. Perhaps I should be replying to a separate thread, but my
questions are:
* What are the goals of minierlang?
* How are these goals different from Erlang?
* What needs to be removed/added from Erlang to make minierlang?
* What is the current VM instruction set, and what would be the Mini
instruction set?
(my reason for posing these questions in this thread)
*** Is there any interest in modeling/specifying the behaviors prior to
implementing?
Regarding implementation, I'm fairly agnostic. One thought is that a
prototype could be written in anything (python, bash, java, go, c,
etc.), and once the design has settled down, then anyone should be able
to go back and rewrite in their language of choice. Should be fairly
simple since there would be design docs, formal specifications, test
suites, etc. Then we could have minierlang runtime
competitions/shootouts ;).
[1] http://lamport.azurewebsites.net/tla/tla.html_______________________________________________
erlangquestions mailing list
[hidden email]
http://erlang.org/mailman/listinfo/erlangquestions


On Tue, Sep 26, 2017 at 5:47 PM, Todd GreenwoodGeer
< [hidden email]> wrote:
> Hi,
>
> 1. Are there existing TLA+ specifications [1] for Erlang?
Not that I know of.
>
> Recent discussions regarding the behavior of messages for local and remote
> processes, the behavior of data in ETS, and the discussion about a new
> minierlang all make me think there would be great benefit in formal
> specifications of Erlang behaviors.
>
> For instance, I've been thinking about writing various widgets for
> distributed applications, each with a well defined TLA+ specification, and
> then starting to compose larger and more interesting applications from them.
>
> My workflow would look like this:
> Write widget spec > impl widget > Write application spec (composed of
> previously spec'd widgets) > impl application > profit!
Now sure about the profit bit at the end.
(write crap, sell it, sell thousands of consulting hours to fix it = profit :)
>
> The runtime behaviors such as message passing, process linking, etc. would
> be the first level that would need specifications... so has this ever been
> tackled?
Years ago  but not in phase with the distribution.
There has always been a bit of gap between reality (C code, and what
it does) and specifications (math, and what it should do). The two are
not the same.
>
> 2. Regarding the minierlang, I'd really like to get involved in this
> project. Perhaps I should be replying to a separate thread, but my questions
> are:
There is no project  just a few people discussion what they would like to see
in a new system.
>
> * What are the goals of minierlang?
My goal would be a tiny kernel  performance is
of secondary importance. Tiny runtime footprint.
> * How are these goals different from Erlang?
The current Erlang is not designed for a small memory footprint.
> * What needs to be removed/added from Erlang to make minierlang?
Remove NIFS binarys ets tables (possibly)
> * What is the current VM instruction set, and what would be the Mini
> instruction set?
Current is BEAM  Mini instruction set unknown.
> (my reason for posing these questions in this thread)
> *** Is there any interest in modeling/specifying the behaviors prior to
> implementing?
I dont' think so  the main problem is figuring out how to make something
with tiny footprint  so for example GC strategy and memory layout is
very important  I don't think modelling helps. Counting bytes on squared paper
seems the best method (really)
>
> Regarding implementation, I'm fairly agnostic. One thought is that a
> prototype could be written in anything (python, bash, java, go, c, etc.),
I disagree  I'd like the final memory footprint to be small.
c (and friends) are OK but I don't want to have to include an entire JVM
(or whatever).
Could implement it in Forth though ...
> and once the design has settled down, then anyone should be able to go back
> and rewrite in their language of choice. Should be fairly simple since
> there would be design docs, formal specifications, test suites, etc. Then we
> could have minierlang runtime competitions/shootouts ;).
That would be fun.
Cheers
/Joe
>
> [1] http://lamport.azurewebsites.net/tla/tla.html> _______________________________________________
> erlangquestions mailing list
> [hidden email]
> http://erlang.org/mailman/listinfo/erlangquestions_______________________________________________
erlangquestions mailing list
[hidden email]
http://erlang.org/mailman/listinfo/erlangquestions


If we're talking about a new instruction set, and removing pieces from the runtime, then are we still talking about a minimal Erlang, or are we talking about something new? Because I'm sure we could all think of thing's we'd change given the opportunity. Joe's already written Erl2.
Brady
On Tuesday, September 26, 2017, 12:36:04 PM EDT, Joe Armstrong < [hidden email]> wrote:
On Tue, Sep 26, 2017 at 5:47 PM, Todd GreenwoodGeer < [hidden email]> wrote: > Hi, > > 1. Are there existing TLA+ specifications [1] for Erlang? Not that I know of. > > Recent discussions regarding the behavior of messages for local and remote > processes, the behavior of data in ETS, and the discussion about a new > minierlang all make me think there would be great benefit in formal > specifications of Erlang behaviors. > > For instance, I've been thinking about writing various widgets for > distributed applications, each with a well defined TLA+ specification, and > then starting to compose larger and more interesting applications from them. > > My workflow would look like this: > Write widget spec > impl widget > Write application spec (composed of > previously spec'd widgets) > impl application > profit!
Now sure about the profit bit at the end. (write crap, sell it, sell thousands of consulting hours to fix it = profit :) > > The runtime behaviors such as message passing, process linking, etc. would > be the first level that would need specifications... so has this ever been > tackled? Years ago  but not in phase with the distribution. There has always been a bit of gap between reality (C code, and what it does) and specifications (math, and what it should do). The two are not the same. > > 2. Regarding the minierlang, I'd really like to get involved in this > project. Perhaps I should be replying to a separate thread, but my questions > are: There is no project  just a few people discussion what they would like to see in a new system. > > * What are the goals of minierlang? My goal would be a tiny kernel  performance is of secondary importance. Tiny runtime footprint. > * How are these goals different from Erlang? The current Erlang is not designed for a small memory footprint. > * What needs to be removed/added from Erlang to make minierlang? Remove NIFS binarys ets tables (possibly) > * What is the current VM instruction set, and what would be the Mini > instruction set? Current is BEAM  Mini instruction set unknown. > (my reason for posing these questions in this thread) > *** Is there any interest in modeling/specifying the behaviors prior to > implementing? I dont' think so  the main problem is figuring out how to make something with tiny footprint  so for example GC strategy and memory layout is very important  I don't think modelling helps. Counting bytes on squared paper seems the best method (really) > > Regarding implementation, I'm fairly agnostic. One thought is that a > prototype could be written in anything (python, bash, java, go, c, etc.), I disagree  I'd like the final memory footprint to be small. c (and friends) are OK but I don't want to have to include an entire JVM (or whatever). Could implement it in Forth though ... > and once the design has settled down, then anyone should be able to go back > and rewrite in their language of choice. Should be fairly simple since > there would be design docs, formal specifications, test suites, etc. Then we > could have minierlang runtime competitions/shootouts ;). That would be fun. Cheers /Joe > > [1] http://lamport.azurewebsites.net/tla/tla.html> _______________________________________________ > erlangquestions mailing list > [hidden email]> http://erlang.org/mailman/listinfo/erlangquestions
_______________________________________________
erlangquestions mailing list
[hidden email]
http://erlang.org/mailman/listinfo/erlangquestions


On Tue, Sep 26, 2017 at 8:22 PM, Brady Powers < [hidden email]> wrote:
> If we're talking about a new instruction set,
Yes
> and removing pieces from the
> runtime,
No  write a new runtime but inspired by and stealing good bits from the old
then are we still talking about a minimal Erlang,
or are we talking
It would be a subset of Erlang  so strictly not Erlang
> about something new?
Yes
> Because I'm sure we could all think of thing's we'd change given the
> opportunity. Joe's already written Erl2.
No  erl2 just compiles to erl
/Joe
> Brady
> On Tuesday, September 26, 2017, 12:36:04 PM EDT, Joe Armstrong
> < [hidden email]> wrote:
>
>
> On Tue, Sep 26, 2017 at 5:47 PM, Todd GreenwoodGeer
> < [hidden email]> wrote:
>> Hi,
>>
>> 1. Are there existing TLA+ specifications [1] for Erlang?
>
> Not that I know of.
>
>>
>> Recent discussions regarding the behavior of messages for local and remote
>> processes, the behavior of data in ETS, and the discussion about a new
>> minierlang all make me think there would be great benefit in formal
>> specifications of Erlang behaviors.
>>
>> For instance, I've been thinking about writing various widgets for
>> distributed applications, each with a well defined TLA+ specification, and
>> then starting to compose larger and more interesting applications from
>> them.
>>
>> My workflow would look like this:
>> Write widget spec > impl widget > Write application spec (composed of
>> previously spec'd widgets) > impl application > profit!
>
> Now sure about the profit bit at the end.
>
> (write crap, sell it, sell thousands of consulting hours to fix it = profit
> :)
>
>>
>> The runtime behaviors such as message passing, process linking, etc. would
>> be the first level that would need specifications... so has this ever been
>> tackled?
>
> Years ago  but not in phase with the distribution.
>
> There has always been a bit of gap between reality (C code, and what
> it does) and specifications (math, and what it should do). The two are
> not the same.
>
>>
>> 2. Regarding the minierlang, I'd really like to get involved in this
>> project. Perhaps I should be replying to a separate thread, but my
>> questions
>> are:
>
> There is no project  just a few people discussion what they would like to
> see
> in a new system.
>
>
>>
>> * What are the goals of minierlang?
>
> My goal would be a tiny kernel  performance is
> of secondary importance. Tiny runtime footprint.
>
>> * How are these goals different from Erlang?
>
> The current Erlang is not designed for a small memory footprint.
>
>> * What needs to be removed/added from Erlang to make minierlang?
>
> Remove NIFS binarys ets tables (possibly)
>
>> * What is the current VM instruction set, and what would be the Mini
>> instruction set?
>
> Current is BEAM  Mini instruction set unknown.
>
>> (my reason for posing these questions in this thread)
>> *** Is there any interest in modeling/specifying the behaviors prior to
>> implementing?
>
> I dont' think so  the main problem is figuring out how to make something
> with tiny footprint  so for example GC strategy and memory layout is
> very important  I don't think modelling helps. Counting bytes on squared
> paper
> seems the best method (really)
>
>>
>> Regarding implementation, I'm fairly agnostic. One thought is that a
>> prototype could be written in anything (python, bash, java, go, c, etc.),
>
> I disagree  I'd like the final memory footprint to be small.
> c (and friends) are OK but I don't want to have to include an entire JVM
> (or whatever).
>
> Could implement it in Forth though ...
>
>> and once the design has settled down, then anyone should be able to go
>> back
>> and rewrite in their language of choice. Should be fairly simple since
>> there would be design docs, formal specifications, test suites, etc. Then
>> we
>> could have minierlang runtime competitions/shootouts ;).
>
> That would be fun.
>
> Cheers
>
> /Joe
>
>
>>
>> [1] http://lamport.azurewebsites.net/tla/tla.html>> _______________________________________________
>> erlangquestions mailing list
>> [hidden email]
>> http://erlang.org/mailman/listinfo/erlangquestions>
> _______________________________________________
> erlangquestions mailing list
> [hidden email]
> http://erlang.org/mailman/listinfo/erlangquestions_______________________________________________
erlangquestions mailing list
[hidden email]
http://erlang.org/mailman/listinfo/erlangquestions


> No  write a new runtime but inspired by and stealing good bits from the old
what would you consider good bits here?
i also suspect that mini erlang would be better off without process dictionaries?
_______________________________________________
erlangquestions mailing list
[hidden email]
http://erlang.org/mailman/listinfo/erlangquestions


General rule when trying to build language cores formally:
Every construction which can be written in terms of another construction should be. * ETS tables are really just processes * The Process dictionary is just a state monad in the language * You need monads for message passing side effects anyway, so you can probably reuse the work on top * The whole exception system can be cast inside the monad as well * Ports can be reimagined as special processes and you can use messaging in order to handle them
The reason is that any construction is a formal liability: it needs special handling. It is often more beneficial to generalize the system a little bit in order to vastly simplify the number of cases you have to handle in proofs.
> No  write a new runtime but inspired by and stealing good bits from the old
what would you consider good bits here?
i also suspect that mini erlang would be better off without process dictionaries?
_______________________________________________
erlangquestions mailing list
[hidden email]
http://erlang.org/mailman/listinfo/erlangquestions
_______________________________________________
erlangquestions mailing list
[hidden email]
http://erlang.org/mailman/listinfo/erlangquestions


Also, it is important that all BIFs that have to do with state outside of the process itself (as opposed to e.g. the process dictionary functions)  such as the process registry functions, system time, timers, etc.  can and should be modelled as messages to and from the corresponding VM subsystem. Yes, this implies a lot of possible race conditions  but these already exist in a modern Beam, where multiple threads are working simultaneously and trying to avoid global locks. Best to get those out in the open right away, so you don't paint yourself in a corner by assuming that certain BIFs always will take effect globally, atomically and instantaneously.
I think this is an underappreciated (or at least not widely understood) property of Erlang and its implementation. You could in fact have large parts of its runtime system execute on a physically separate machine from the processes that run your Beam code, without having to change a line in your programs.
_______________________________________________
erlangquestions mailing list
[hidden email]
http://erlang.org/mailman/listinfo/erlangquestions


In reply to this post by Jesper Louis Andersen2
Hi Jesper,
Can you please enlighten me (Erlang newbie here) about this “Monad” things. I’ve heard this word multiple times and still can’t get it.
To me, It’s kind of magic word you say to impress people, and let them think you know functional programming very well 😉
A simple, concrete example will be more than welcome.
Thanks /Frank General rule when trying to build language cores formally:
Every construction which can be written in terms of another construction should be. * ETS tables are really just processes * The Process dictionary is just a state monad in the language * You need monads for message passing side effects anyway, so you can probably reuse the work on top * The whole exception system can be cast inside the monad as well * Ports can be reimagined as special processes and you can use messaging in order to handle them
The reason is that any construction is a formal liability: it needs special handling. It is often more beneficial to generalize the system a little bit in order to vastly simplify the number of cases you have to handle in proofs.
> No  write a new runtime but inspired by and stealing good bits from the old
what would you consider good bits here?
i also suspect that mini erlang would be better off without process dictionaries?
_______________________________________________
erlangquestions mailing list
[hidden email]
http://erlang.org/mailman/listinfo/erlangquestions
_______________________________________________
erlangquestions mailing list
[hidden email]
http://erlang.org/mailman/listinfo/erlangquestions
_______________________________________________
erlangquestions mailing list
[hidden email]
http://erlang.org/mailman/listinfo/erlangquestions


In this setting, Monads are used subtly different from the more "normal" setting, but I'll try to draw the connection anyway.
When you are trying to formalize a programming language, there is a list of effectful constructions we may want to add to the language:
* Exceptions or Process Crashes * State or the Process Dictionary * Communication patterns * Hibernation (or more generally: continuation constructs) * Nondeterministic computation * ...
The list goes on and also includes more "esoteric" constructions such as variables which has a certain value with a probability, quantum computations, computations where state flows in the reverse order of the program and so on.
If we add these constructions to a programming language and wish to formalize the language so we can prove theorems about it, then the language can easily become quite large very quickly. This hampers our proofeffort since we need to address the added complexity in all proofs we are doing. Exceptions will mean we have to address the concepts of "throw" and "handle". State will mean we have to address what "put" and "get" does and so on. More importantly, we will have to alter the whole semantics since now there are state and added control flow to keep track of!
But there is hope. A nontrivial insight is that all the above constructions have something in common. We can, so to speak, extract a more general notion of the above. This is good, because if we can prove something in generality, we can "plug in" the specifics exceptions, the state and so oninto our proof. We don't have to handle everything up front if this works out. The price is that the general notion might be harder to work with in the first place.
You can then ask: what should the rules of such a general notion be? It turns out mathematicians working in the area of Category Theory already had a definition which fit: the Monad. Remarkably, this creates a link, so to speak, between mathematics and programming languages. We can capture the above needed generality by observing that what they have in common are the "Monad Laws".
Hence our task, as formal semanticists, can now be changed and we can attack the problem in another way:
1. Show that we can add an abstract Monad to our language. Since the abstraction must hold for every possible monad, we are thus only allowed the use of the Monad Laws when dealing with proofs about the language.
2. Show that Exceptions, State, ... obeys the Monad laws.
3. Plug the things together to obtain a language which is extended with the effects of our desire.
The hope is that dealing with 1 and 2 separately is easier than dealing with both at the same time.

The other common use of a "Monad" is to embed effects into a pure language. This idea goes back to Moggi (I believe) and was popularized by Phil Wadler for Haskell[0]. Here the Monad acts like a stratification: computations are put into classes depending on what effects they have. E.g., "exceptions goes here", "io computation goes there" and so on. The key insight is that we can thus keep computations with effects apart from (pure) computations without. Even more interesting, because Haskell is a statically typed language, we can enforce that computations with different effects cannot accidentally be mixed in wrong ways. This helps with correctness.
What makes the monad construction hard to grasp initially is that it is an abstract notion in line with recursion. One has to work with it for a while to build up a certain amount of familiarity with the concept. This is also why it is so hard to explain: most tutorials are giving you a glimpse of the real deal through metaphor and analogy in the hope that it can make your mind think in the right way. But in reality it is just a definition of a mathematical object with certain laws. Why exactly *those* laws and not something else? Well it turned out that these laws were the useful ones[1]. Why the link to computer science? Because the universe is a remarkable place of systems.
[0] Phil's original paper is one of the best expositions of the idea and still to this day is one of the most readable.
[1] Mathematicians some times call such laws the "natural laws" in the sense that they afford you the most power from a perspective of using the definition as a building block for further work.
Hi Jesper,
Can you please enlighten me (Erlang newbie here) about this “Monad” things. I’ve heard this word multiple times and still can’t get it.
To me, It’s kind of magic word you say to impress people, and let them think you know functional programming very well 😉
A simple, concrete example will be more than welcome.
Thanks General rule when trying to build language cores formally:
Every construction which can be written in terms of another construction should be. * ETS tables are really just processes * The Process dictionary is just a state monad in the language * You need monads for message passing side effects anyway, so you can probably reuse the work on top * The whole exception system can be cast inside the monad as well * Ports can be reimagined as special processes and you can use messaging in order to handle them
The reason is that any construction is a formal liability: it needs special handling. It is often more beneficial to generalize the system a little bit in order to vastly simplify the number of cases you have to handle in proofs.
> No  write a new runtime but inspired by and stealing good bits from the old
what would you consider good bits here?
i also suspect that mini erlang would be better off without process dictionaries?
_______________________________________________
erlangquestions mailing list
[hidden email]
http://erlang.org/mailman/listinfo/erlangquestions
_______________________________________________
erlangquestions mailing list
[hidden email]
http://erlang.org/mailman/listinfo/erlangquestions
_______________________________________________
erlangquestions mailing list
[hidden email]
http://erlang.org/mailman/listinfo/erlangquestions


Jesper: many thanks again for taking time explaining the Monad concept in this specific case and in general.
I found this module and I’ll try to play with it:
/Frank
In this setting, Monads are used subtly different from the more "normal" setting, but I'll try to draw the connection anyway.
When you are trying to formalize a programming language, there is a list of effectful constructions we may want to add to the language:
* Exceptions or Process Crashes * State or the Process Dictionary * Communication patterns * Hibernation (or more generally: continuation constructs) * Nondeterministic computation * ...
The list goes on and also includes more "esoteric" constructions such as variables which has a certain value with a probability, quantum computations, computations where state flows in the reverse order of the program and so on.
If we add these constructions to a programming language and wish to formalize the language so we can prove theorems about it, then the language can easily become quite large very quickly. This hampers our proofeffort since we need to address the added complexity in all proofs we are doing. Exceptions will mean we have to address the concepts of "throw" and "handle". State will mean we have to address what "put" and "get" does and so on. More importantly, we will have to alter the whole semantics since now there are state and added control flow to keep track of!
But there is hope. A nontrivial insight is that all the above constructions have something in common. We can, so to speak, extract a more general notion of the above. This is good, because if we can prove something in generality, we can "plug in" the specifics exceptions, the state and so oninto our proof. We don't have to handle everything up front if this works out. The price is that the general notion might be harder to work with in the first place.
You can then ask: what should the rules of such a general notion be? It turns out mathematicians working in the area of Category Theory already had a definition which fit: the Monad. Remarkably, this creates a link, so to speak, between mathematics and programming languages. We can capture the above needed generality by observing that what they have in common are the "Monad Laws".
Hence our task, as formal semanticists, can now be changed and we can attack the problem in another way:
1. Show that we can add an abstract Monad to our language. Since the abstraction must hold for every possible monad, we are thus only allowed the use of the Monad Laws when dealing with proofs about the language.
2. Show that Exceptions, State, ... obeys the Monad laws.
3. Plug the things together to obtain a language which is extended with the effects of our desire.
The hope is that dealing with 1 and 2 separately is easier than dealing with both at the same time.

The other common use of a "Monad" is to embed effects into a pure language. This idea goes back to Moggi (I believe) and was popularized by Phil Wadler for Haskell[0]. Here the Monad acts like a stratification: computations are put into classes depending on what effects they have. E.g., "exceptions goes here", "io computation goes there" and so on. The key insight is that we can thus keep computations with effects apart from (pure) computations without. Even more interesting, because Haskell is a statically typed language, we can enforce that computations with different effects cannot accidentally be mixed in wrong ways. This helps with correctness.
What makes the monad construction hard to grasp initially is that it is an abstract notion in line with recursion. One has to work with it for a while to build up a certain amount of familiarity with the concept. This is also why it is so hard to explain: most tutorials are giving you a glimpse of the real deal through metaphor and analogy in the hope that it can make your mind think in the right way. But in reality it is just a definition of a mathematical object with certain laws. Why exactly *those* laws and not something else? Well it turned out that these laws were the useful ones[1]. Why the link to computer science? Because the universe is a remarkable place of systems.
[0] Phil's original paper is one of the best expositions of the idea and still to this day is one of the most readable.
[1] Mathematicians some times call such laws the "natural laws" in the sense that they afford you the most power from a perspective of using the definition as a building block for further work.
Hi Jesper,
Can you please enlighten me (Erlang newbie here) about this “Monad” things. I’ve heard this word multiple times and still can’t get it.
To me, It’s kind of magic word you say to impress people, and let them think you know functional programming very well 😉
A simple, concrete example will be more than welcome.
Thanks General rule when trying to build language cores formally:
Every construction which can be written in terms of another construction should be. * ETS tables are really just processes * The Process dictionary is just a state monad in the language * You need monads for message passing side effects anyway, so you can probably reuse the work on top * The whole exception system can be cast inside the monad as well * Ports can be reimagined as special processes and you can use messaging in order to handle them
The reason is that any construction is a formal liability: it needs special handling. It is often more beneficial to generalize the system a little bit in order to vastly simplify the number of cases you have to handle in proofs.
> No  write a new runtime but inspired by and stealing good bits from the old
what would you consider good bits here?
i also suspect that mini erlang would be better off without process dictionaries?
_______________________________________________
erlangquestions mailing list
[hidden email]
http://erlang.org/mailman/listinfo/erlangquestions
_______________________________________________
erlangquestions mailing list
[hidden email]
http://erlang.org/mailman/listinfo/erlangquestions
_______________________________________________
erlangquestions mailing list
[hidden email]
http://erlang.org/mailman/listinfo/erlangquestions

