[lambdasquirrel]

And yet it all circles back.

We used Peano arithmetic when doing C++ template metaprogramming anytime a for loop from 0..n was needed. It was fun and games as long as you didn't make a mistake because the compiler errors would be gnarly. The Haskell people still do stuff like this, and I wouldn't be surprised if someone were doing it in Scala's type system as well.

Also, the PLT people are using lattices and categories to formalize their work.