Fwd: Re: Maude licensed under GPL, 2.0 approaching

[Alexis Read]

On Mon, 2 Jun 2003, Massimo Dentico wrote:

>
> As suggested by Brian, I forward this private e-mail exchange to the list=
,
> only sligltly edit and purged of details not relevant here. Follow in
> another post his replay.
>
> ------------------- Forwarded message -----------------------------------=
-
> From: "Massimo Dentico" <m.dentico@virgilio.it>
> To: "Brian T Rice" <water@tunes.org>
> Sent: Monday, June 02, 2003 1:25 AM
> Subject: Re: Maude licensed under GPL, 2.0 approaching
>
> Hello Brian,
>
> thanks for this update on Maude development status.
>
> I'm curious: there is a private mailing list for developers only?
>

there is a subscribers list- see the website.
http://maude.csl.sri.com
> [..]
>
> My idea for a next step for Tunes is to advance in parallel different
> aspects of the system:
>

All of maude is useful. It IS possible to express the whole of maude
within itself - see the online manual where it talks about a universal
theory U that includes itself (this is mathematically demonstrated as
well). Bootstrapping will depend on what is in maude 2.0 -i haven't looked
yet but i think there's a compiler, if so then very possible.
a) Maude captures the concept of rewriting relatively completely as is
known so far (mathematically), BOBJ extends the concepts in useful
directions (both languages are in the same family).
I'm not quite clear on what you mean by abstracting from the nature of
base objects - maude supports user defined types and proofs on those
types, BOBJ can do proofs on black-box code and other behavioral objects
which is about as good as you can hope to get without a brain like
newton's/einstein's etc.

b) maude can already do this - most circuits are designed in VHDL which is
a more primative precursor to maude. You can even probably write a
specification translator to move the hardware spec across to maude.

c) See any of the maude tutorial examples to see how this can be done.

3) This is a topic to look at once a start has been made surely :o)

Maude will always be useful as it has solid math foundations for the
language, it is to my knowledge the most state of the art system available
and there are a few choices (most of them in the same language family).
BOBJ runs a close second, and the algorithms need to be incorporated into
maude.
Alexis

> 1) to explore what we can "steal" from Maude as high level declarative
>    language and what to change or inject to approach Tunes ideas;
>
> 2) how to express Maude implementation in Maude itself or how to bootstra=
p
>    our Maude/Tunes (M/T from now), or:
>
>    a) how to express in M/T the transformation from term rewriting
>       to BDD (I don't know if this makes sense: I'm speaking without
>       a true knowledge of the Maude implementation). In case for M/T
>       we can research how to go beyond term (or graph/string/whatever)
>       rewriting and capture the concept of rewriting in general,
>       abstracting from the nature of base objects with our abstract
>       notion of object (or someone have done this already?);
>
>    b) how to model low level (machine) entities, beginning from the CPU,
>       in M/T;
>
>    c) at last, how to map the transformation in a) in terms of entities
>       in b);
>
> 3) co-evolving the spec with feedback from 1) and 2).
>
> Note that in a) the underlying assumption is that the implementation of
> Maude is state of the art wrt rewriting systems but I'm absolutely
> conscious that, for the nature of the system itself, this choice is not
> mandatory.
>
> I remember also a list of "experiments" (in and about Tunes) in a
> e-mail by Far=E9 on the LL1 mailing list but I have not a reference
> at hand. IIRC, some are about self-organization, emergent properties
> and alike. On the subject I don't know if you have noticed that parts
> of Maude are to be used in ADATE's successor, see bottom of page of:
>
>   http://www-ia.hiof.no/~rolando/adate_intro.html
>
>
> This is only a rough sketch, just to start a discussion: some parts are
> missing, other are trivialized.
>
> Of course we need to show how better, wrt other usual approaches, all thi=
s
> stuff actually solves real problems.
>
> ------------------- End of forwarded message ----------------------------
>
> Regards.
>
> --
> Massimo Dentico
>
>
>