Re: Magic, Oracles, tomatos, and meaning questions not to ask

[Daniel Hagerty <hag @ linnaean . org>]

 >  	Ok.  To summarise, "magic" is the above plus other,
 > yet-to-be-defined stuff :).  Yes?  No?

    "Yes".  We will avoid the "other" category as irrelevant for now.

 >  	By configuration, I mean a "program" written in the above
 > language.  Although in a networks context, program usually specifies
 > desired state rather than a series of actions (sorry, proceduralist here
 > :) ).

    You allude to the difference between imperitive and declaritive
forms of communication.  "Stand up!" versus perhaps "Proper people
stand up in this situation.  You are a proper person."

    Math is the land of the declarative.  I don't care if you chose to
speak an imperitive language if your problem is better said as such.
HOWEVER, we must be able to express your imperitive as the declaration
of a side effect within a mathematical world if I have any hope of
reasoning with it.  This is what the scheme semantic does, for
example.  There are expressible side effects, but the result of a side
effects is a value, not a side effect.

    As to questions like "does some oracle approach require a full
semantic of perl", no, that would be hopeless.  The non-tractability
of things like full perl interpreters or human beings is something you
go out of your way to *avoid* explaining.  If your system requires you
explain such a thing, your system is probably wrong.

    Of course, sometimes you can't avoid explaining something
ridiculous, like the various hideous scenarious brought up in
rollback of devices with no real support of it.  Sometimes, it sucks
to be you.

    Would you rather hide the semantic implied by your program within
a general purpose language, or would you like to expose the horror of
the semantic in all its unglory and use this information as data
within your program?

    I would ask that you do the latter if you want to share this
information with me.  A program in foobar is good too, but not as
good.

 >  	Ok, so I guess my "Language X" above is equivalent to a
 > definition of f(), my "implementation" above is an implementation of f(),
 > and my "configuration" above is equivalent to "sense".  I'm glad to hear
 > my configuration makes sense :-} (<-- evil grin).

    Semantic approaches use more seperation than you seem to indicate.
You speak of a single function application, when in a denotational
world of the sort I'm speaking of, your desired effect involves more
than one application (perhaps many more).

    In a world such as my own, your Language X example as originally
used probably looks something like:

denoted = f(sense-in-X, language-X)
cisco-cfg = f(denoted, reify-cisco-config)
juniper-cfg = f(denoted, reify-juniper-config)

where the key point in what I do is that I only write f once.  It
could be said that what this "really" says (I'm handwaving away a lot)
is:

denoted = language-X(sense-in-X, language-X)
cisco-cfg = reify-cisco-config(denoted, language-X)
juniper-cfg = reify-juniper-config(denoted, reify-juniper-config)

    It is important to note that functions like language-X and
reify-cisco-config are written by users.  I write f and supporting
infrastructure.

    A real process will probably involve a great deal many more
applications of f, in parts like language-X, reify-cisco-config, and
how you put all these parts together into still broader things to
produce "and configure my cisco router please".  If what you do needs
config fragments sometimes rather than whole configs, nothing prevents
you from factoring thusly.  If fact, denotational semantic approaches
encourage such factoring.


    And now for the "fine print":

The last "program" I wrote as a "proof" of f was:

denoted = f((5, 7), greatest-common-denominator)

    This is *much* simpler than the others, but then, that's the
point.  If I can't make gcd, I can't possibly make bigger things like
a network, or a generalized language to deploy a distributed system
into development, staging, and producting systems, or any number of
other tools I desperately want (*).  Build small, and work up.  I'm
limited by copious free time (**).


    At this level of primitive, the "models" we like to speak of here
don't exist.  Such models are something you make from the more
primitive mathematics we have on hand.

    You need a few magic primitives:

* eval (aka f)
* a denoted locator language
* a denoted definer language
* a bunch of locatable denoted primitives, like arithmetic operators,
  etc.

There are no doubt some more key parts, but that what's playing with
the basics as I am is for.  Once you have a good basis, you try to
build upward.

 >  	Ok, I'm missing these last two bits.  What are our "established
 > mathematical tools"?  Are they currently existing languages like Cisco's
 > IOS config language?

    Sadly, no, we're at a much higher order of "the tools don't seem
to be there".  I speak of the Scott Strachey semantic approach, as an
example.  It expects that your question is of the form
denoted = f(sense)
and as I've demonstrated, our questions are not.  Scott Strachey is
the most rigorous and general denotational semantic system I am aware
of, and it isn't sufficient to do what we seem to need in any graceful
way.  We have hammers & chisels, and we can always make our problem
fit in it, but, um...


    I would like to tell you that the mathematical background was
better than this.   A point can certainly be against my lack of
qualifications to speak of the math: I've got an american public high
school degree of sub-spectacular performance to speak of.  I did not
arrive at being able to speak of what I speak of by choice.


    I've been wandering around many places, include what is now MIT
CSAIL for a long time now, and the smart people there can't tell me
good news as my questions become ever more pointed.  I'm obviously a
net.kook, but despite this, the welcome matt is out for me in many
such places barring copious free time.


(*) There will be a lot of magic to work out, but one of the
gratuitous tricks that's "perfectly tractable" is to:

1. Write the "level 0" denoted interpreter in scheme.
2. Write the system again in denoted. (probably required sooner or
				      later for "long story" reasons)
3. write a "denoted->perl" compiler in denoted.
4. Apply the denoted->perl compiler to denoted.

and what you get is a denoted interpreter, in perl.

This is down there on the list, but is supposed to be doable; if this
isn't doable, something is supposed to be wrong with the math (as this
doesn't involve asking about the meaning of perl, but unparsing into
it, perfectly doable).


As I've said before, if you want to talk to me offline, especially to
see actual code or whatever, feel free to ask.  I haven't made much
code, but your specifics are always wonderful to think about.

(**) But I obviously have time to blather on this mailing list.  It
could be said that writing on mailing lists thusly is actually part of
the process of writing f.