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

[Joe Armstrong]

On Tue, Sep 26, 2017 at 5:47 PM, Todd Greenwood-Geer
<t.greenwoodgeer@REDACTED> 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
> 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!

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 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:

There is no project - just a few people discussion what they would like to see
in a new system.


>
> * What are the goals of mini-erlang?

My goal would be a tiny kernel - performance is
of secondary importance. Tiny run-time 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 mini-erlang?

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 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 ;-).

That would be fun.

Cheers

/Joe


>
> [1] http://lamport.azurewebsites.net/tla/tla.html
> _______________________________________________
> erlang-questions mailing list
> erlang-questions@REDACTED
> http://erlang.org/mailman/listinfo/erlang-questions