[Infrastructures] state machines

Daniel Hagerty Daniel Hagerty <hag@linnaean.org>
Tue, 19 Sep 2006 05:53:07 -0400


    I'm supposed to be avoiding thought at present.  Shame on you!

 > Dan, there's got to be some general way of saying this; I think while
 > either lambda calculus or turing machines can *illustrate* it, they
 > still don't say *why*.

    Turing machines aren't actually used for anything outside of "such
and such is provably turing equivelent, and this, that, and the other
theorem have been proven w.r.t. turing machines".

    Lambda calculus is provably turing equivelent (surprise), and more
expressive to the point that several programming languages
(e.g. scheme, ML, haskell) are thinly veiled lambda calculus.  It's
what's most commonly used for real work of this sort.


    As to the question at hand, you probably aren't going to get the
illustration you want.  The problem is one of practicality, rather
than actual mathematical intractability.  The pie in the sky "what we
want" won't be practical for some time, as opposed to being
impossible.  Counter examples exist, if you look for the right thing.

    Haskell is the most direct citation that leaps to mind.  It's a
purely functional language (no first order side effects), and yet:

* It can express non-terminating programs
* It's compilable in sub-infinite time
* Programs can behave in a non-functional fashion, even though they
  can't be written in anything other than a functional form.

    (none of these are surprising properties)

    In particular, it's worth noting the resemblance of their problems
to what we want:

* A haskell compiler has to process a declaration of a program, and
  produces imperative instructions that mutate the state of a machine
  forward in time so that the machine behaves as the program states.
  As usual, the real problem here is having the programmer understand
  the meaning of what they wrote.
* Haskell debuggers tend to work backwards in time; you often work
  backwards from the result that you don't like to discover how
  behavior disagrees with what you meant.

    This forward and backward in time thing should sound familiar.

    I could probably come up with other related bits, but hopefully
the example above is a good one without going too far afield.

    As for system administration configuration management itself:

    If all we want to do is declare the state of the system and
produce the correct statements to do and undo things in known state,
that's not terribly hard -- the testing isn't really any different
than the more general problem that any software developer faces (and
yes, this is a handwave, in that most software testing isn't up to the
level of required rigor).  People are able to do this now when they
cut the problem up and declare certain things out of scope.

    If we're looking to work from unknown state (in other words, step
1 being discover the current state), the problem varies between
obscenely hard, and intractible.  There's a lot more area on the
"obscenely hard (to the point of impractical)" side of the curve than
the intractible side as far as any "practical" use is concerned.
"rm -rf /; reboot; rollback" falls closer to the intractible side.
There's more handwaving in here that requires proper qualifications.


    Anyway, discuss.  I know you disagree with me on the substance of
this.  Varying degrees of proof take more work and are more likely to
come out of being called out on my BS.  It's past bedtime for bozo.