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

[Joe Armstrong]

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