Last week, I found Jeremy Wertheimer's master thesis from MIT; Derivation of an efficient rule system pattern matcher. It seems very interesting. He derives a Rete implementation using program transformations (in the programming language Refine which seems to be some Lisp dialect or other). Apparently he starts out with a small formal specification of Rete and applies transformations to it step by step in order to derive an efficient pattern matcher. Very cool.