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

Fri Oct 6 23:56:09 CEST 2017

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.

        /Richard

2017-10-06 20:07 GMT+02:00 Jesper Louis Andersen <
jesper.louis.andersen@REDACTED>:

> 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.
>
>
> On Wed, Sep 27, 2017 at 7:20 AM Karlo Kuna <kuna.prime@REDACTED> wrote:
>
>> > 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?
>>
>>
>>
>> On Tue, Sep 26, 2017 at 10:59 PM, Joe Armstrong <erlang@REDACTED> wrote:
>>
>>> On Tue, Sep 26, 2017 at 8:22 PM, Brady Powers <powers_brady@REDACTED>
>>> 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
>>> > <erlang@REDACTED> wrote:
>>> >
>>> >
>>> > 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
>>> >
>>> > _______________________________________________
>>> > erlang-questions mailing list
>>> > erlang-questions@REDACTED
>>> > http://erlang.org/mailman/listinfo/erlang-questions
>>> _______________________________________________
>>> erlang-questions mailing list
>>> erlang-questions@REDACTED
>>> http://erlang.org/mailman/listinfo/erlang-questions
>>>
>>
>> _______________________________________________
>> erlang-questions mailing list
>> erlang-questions@REDACTED
>> http://erlang.org/mailman/listinfo/erlang-questions
>>
>
> _______________________________________________
> erlang-questions mailing list
> erlang-questions@REDACTED
> http://erlang.org/mailman/listinfo/erlang-questions
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://erlang.org/pipermail/erlang-questions/attachments/20171006/2a2b0c57/attachment.htm>