BackMath: a compile time symbolic math lib.

[BCS]

I have written a library that allows for all of the following as native syntax:

A + B - D = C;
A - B - D = C;
A - D - B = C;
(B - A) - D = C;
A - D - B - D = C;
A - B - (D + D) = C;
C = A + B - D;
C = B * A;
C = B * A + B * D;
A / B  + D / B = C;

In all of these cases the assignment is to B.

The library is works by using term re-writing to reverse evaluate the expression. 
The fun part is that the term re-writing is done with the type system and 
template expressions. This results in there being little inherent runtime 
cost.
I hope to expand it to work with as wide a variety of equation forma as I 
can. I wold love to be able to get it to even solve system of equations like

a*B + c*D = e;
f*B + g*D = h;

where B and D are both unknown.

Now, full disclosure:
-it's incomplete, there a lots of cases it won't handle (but I plan on improving 
that)
-it is not thread safe, this is because the templates need alias to variables 
to work correctly and the only variables that can be aliased are globals.*, #
-It's unproven, I can formally prove all the "single sided" rules, but haven't 
figured out how to prove the "double sided" rules, yet like the last 2 examples, 
%
-No, I didn't bang out 400 lines of static if's, the "business logic" is 
generated using a lisp program that is harder to read than what it produces ^

Now for the challenge. Is anyone willing to try and generate a C++ equivalent? 
I think it would be really cool to have a side by side comparison of the 
two libs. I think the difference in readability say a lot.

hosted at:
   http://www.dsource.org/projects/scrapple/browser/trunk/backmath

* Walter can we please get this fixed??
# I have a way in mind to fix this but it won't look near as good.
% I'm using ACL2 to do the proofs. http://www.cs.utexas.edu/users/moore/acl2/
^ I'll clean it up and post it as well soon. (finals week is coming soon 
so don't hold your breath or anything)