Hi all, author of the website here (I'm <a href="https://johannes-bader.com/" rel="nofollow">https://johannes-bader.com/</a>). Wow, thanks for the reactions and many good suggestions! I thought I'd add a bit of context here.<p>As has correctly been pointed out, Tree Calculus was developed by Barry Jay! The "Specification" page links to his book. And a preview of his PEPM 2025 paper (hi chewxy!) can now be found here: <a href="https://github.com/barry-jay-personal/typed_tree_calculus/blob/main/typed_program_analysis.pdf">https://github.com/barry-jay-personal/typed_tree_calculus/bl...</a><p>Compared to how long Barry has been professionally researching this, I entered the picture yesterday and joined the effort to help. Potential mistakes on the website are mine, not Barry's, but I do firmly believe in some of the "ambitious" wording there. Blog posts and more concrete demos or details to come!<p>Just for the curious, here is my angle in all this:<p>I happened to (hobbyist!) research tiny, yet practical, languages for over a decade (see e.g. <a href="https://lambada.pages.dev/" rel="nofollow">https://lambada.pages.dev/</a>). In that work I started noticing that the Iota combinator (<a href="https://en.wikipedia.org/wiki/Iota_and_Jot" rel="nofollow">https://en.wikipedia.org/wiki/Iota_and_Jot</a>) is not a combinator in the most traditional sense: It is usually defined as behaving like "\x x S K", but like, how can we just refer to a lambda in the <i>definition</i> of a logic? One could write reduction rules such as "Iota Iota x -> x", but now Iota appears on the left hand side, in argument position! Doesn't that allow reflecting on arguments? Horror! I just started realizing that, while SK is perfectly Turing complete and sane, forcing down the number of combinators from 2 to 1 magically forces some amount of intensionality! Curious, isn't it?<p>And that's when I came across Barry's work and book! A calculus that embraces intensionality. So I reached out to see if I can help. How can I be most useful? Barry has been figuring out theory, professionally, before I could think. So I felt like helping spread the word, maybe to a less academic developer crowd, would be a more effective way to contribute. I spent my entire career building developer tools, so I have some ideas what could be useful and what might be necessary to convince various kinds of developers. That's how the website came to be, and it is very much a work in progress. We sync regularly, for instance Barry had excellent ideas for demos and I suggested slightly tweaked reduction rules at some point (not more powerful in theory, just more convenient in practice), see "triage calculus" in typed_program_analysis.pdf