[erlang-questions] Erlang, mini-erlang, and TLA+
Tue Sep 26 17:47:59 CEST 2017
1. Are there existing TLA+ specifications  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 mini-erlang 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
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 mini-erlang, I'd really like to get involved in this
project. Perhaps I should be replying to a separate thread, but my
* What are the goals of mini-erlang?
* How are these goals different from Erlang?
* What needs to be removed/added from Erlang to make mini-erlang?
* What is the current VM instruction set, and what would be the Mini
(my reason for posing these questions in this thread)
*** Is there any interest in modeling/specifying the behaviors prior to
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 re-write in their language of choice. Should be fairly
simple since there would be design docs, formal specifications, test
suites, etc. Then we could have mini-erlang runtime
More information about the erlang-questions