STsteego·Apr 9, 2026
For people wondering what this is and whether to take this seriously, I’ll try to provide some context:
Tree Calculus is a novel alternative to lambda calculus as a minimal model of computation. Unlike most minimal systems, tree calculus is fundamentally capable of being fully reflective.
If you were ever interested in creating a programming language that could fully reflect and enhance itself with libraries, this is one of a very few number of known minimal system you can use as a starting point. Think of it as a lambda calculus with macros built into the underlying calculus, not something bolted on afterward based on a partially implemented meta-theory.
If you’re into formal proofs, you can find Rocq proofs of his work in his repo.
https://github.com/barry-jay-personal/tree-calculus
If you’re interested in how something like tree calc
Read the rest
ulus can express a type system, here’s a recent ACM paper:
https://dl.acm.org/doi/pdf/10.1145/3704253.3706138
Personal context, Barry Jay is a respected academic and researcher who’s collaborated with people like Simon Peyton Jones and Eugenio Moggi. His PhD advisor was Joachim Lambek (from the Curry-Howard-Lambek correspondence). He’s not a random professor with a neat toy, Barry’s been working with many of the best minds on the foundations of computation long before most of us knew category theory existed. He’s been formalizing and defining pattern matching, higher-ordered patterns and has been searching/separating what is truly essential from what is not essential for decades.
Seriously, look at his research history on Google Scholar.
I think it will take the rest of us a while to understand and unpack the insight he’s already imbued into such a small and simple calculus.