Lambda the Ultimate

I posted a while ago about a meta-circular Javascript interpreter I've been working on (now called Tailspin).

It is now reversible. As well as running in the browser and allowing algorithms to be visualised, Tailspin can now run code both forwards and backwards (using lots of continuations).

Being reversible provides some really interesting opportunities for exploring program execution and aiding learning to code. So far I have focused on algorithm visualisation where reversibility makes it possible to scrub through the execution of algorithms. This is not just fun, it transforms the experience of understanding the algorithm. I've been surprised at how simple it has been to create some really good visualisations (see the wiki), it's a little hacky at the moment, but it's really easy using the wiki to create an algorithm visualisation and without any work to be able to scrub back and forth through it.

Suggestions for uses or improvements are very welcome.


More info: http://will.thimbleby.net/reversible-javascript/
Wiki: http://will.thimbleby.net/algorithms
IDE: http://will.thimbleby.net/algorithms/inspector

I'm not sure I know what I'm talking about...

Isn't dimensional analysis used in natural science a kind of type checking? If so, doesn't it mean Curry–Howard isomorphism is applicable and, therefore, dimensional analysis is simply theorem proofing?