Very cool. This actually intensely reminds me of Ed Yang's logitext sequent calculus tutorial: http://logitext.ezyang.scripts.mit.edu/logitext.fcgi/tutoria...

You don't have to know the rules of the sequent calculus, you can just click around, but the theorem prover will ensure that you can't break them. Then, by fucking around and reading through the tutorial, you can pretty much learn how it works.

I think that things like this are the right way to start designing interactive education. Create a play space, enforce the rules, provide lessons that act as hints and tips for understanding how the rules work.