formal specifications

[RE01 Rice Brian T. EM2]

i'm now going to change the perspective from arrows to Tunes ("finally!"
everyone sighs).  let's come up with some sort of criteria for the kinds of
abstract relationships (patterns) in Tunes that we want to formalize.  i can
think of quite a few which are obvious from my view of the project's goals.
here's a few:

	lambda abstraction in all kinds of ways, for functional /
object-oriented expressions.  everyone here can agree that a Scheme-like
system already encapsulates most of this for us.  i think that we will
probably go 'all the way' by using reflection to reason about the interface
we're using, which most Lisp implementations don't approach.
	abstraction of 'point of view':  we want, via reflection, to say
that such-and-such object represents our current implicit state (our
assumptions, including user-interface etc.) and to use operations which
change that state.  this is what the 'mu' operator i once mentioned was
about.  it's supposed to describe 'fixed-point logic' in a dynamic logic
system.  a dynamic logic is one where you reason about changes in
assumptions that people make as they receive information updates, and the
fixed point idea is to construct an information system at one of the places
between transitions in knowledge.
	the aspect-orientation of any abstraction: we want to be able to
make a Meta-Object Protocol for some group of things that we're describing
to the computer, and then refine it by separating out some issue was
previously implicit in the protocol.  this sounds like something that only
the user could do, from our current perspective.  however, we might be able
to formalize it so that the computer could help us with the process or
verify our work.  we might even run into the conclusion that even
abstraction itself is only an aspect of what we do as users.

this needs some work, of course.  any takers?