[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: [rohc] Formal notation, what is it?



> The point is that, I believe the notation should be about....
> .....notating, nothing else.

Correct.

Now, I did make the proposal that the notation should best be founded on
an executable language ("programming language").  The reason for this was
that previous attempts at defining a notation all had semantic problems.
We needed to map it to *some* CS concepts in a semantically unambiguous
way.  A programming language has the nice property that it allows you to
provide the mapping together with the concepts that you map to.  Not any
programming language will do here -- you need one that allows defining
what amounts to new syntax as well as reasoning about its own programs --
that's why we came up with Prolog and Haskell as two examples (Lisp would
be fine, too, but probably too verbose).

> Note that the notation itself would not be something that would be
> implementable. Of course, the various mechanisms described by the
> notation could be implemented, but not the notation itself. The notation
> is not a machine, it is a language. To me it therefore makes no sense
> to say that "the notation executes", or "the notation calls".

This is, of course, a fine line.  Using a notation language that is rooted
in a programming language and supplying the glue means that the notation
would actually be executable.  As Richard has explained, the resulting
program would not necessarily be very useful without some additional
functionality (e.g., oracles).  It will have a defined execution
semantics, though, and this is the whole point -- it saves us from having
to rigorously define the notation semantics in English, which is a much
worse language for this purpose.  (We do have to give *some* English
language definition, because the notation should be reasonably useful to
those that did not study its foundation in the chosen language.)

Also, we actually can run test cases against the notation and see what
they do.  A really great tool during development of a profile.

All this would be futile if we needed multi-year development efforts to
develop the notation and its programming language mapping.  It seems,
though, that something useful can be built in a much shorter time.  I did
a useful Prolog prototype (some 50 lines!) in a few hours in Atlanta.
Roke Manor did a much more complete Haskell prototype which is still quite
manageable.  These prototypes have enormously helped in communicating
about the  properties of the notation that we consider desirable or
undesirable.  Even if we go back to English-language-only standardization
of the notation, the current work will have been tremendously useful.

Gruesse, Carsten
_______________________________________________
Rohc mailing list
Rohc@ietf.org
https://www1.ietf.org/mailman/listinfo/rohc