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

[Jesper Louis Andersen]

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
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://erlang.org/pipermail/erlang-questions/attachments/20171006/af3f06d6/attachment.htm>