[erlang-questions] Erlang, mini-erlang, and TLA+

[Todd Greenwood-Geer]

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 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 
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 mini-erlang, 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 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 
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 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 
competitions/shootouts ;-).

[1] http://lamport.azurewebsites.net/tla/tla.html