[Karrot_Kream]

I guess I'm confused as to why this is more than simply an interesting formalism. Complexity theory and models of computation are largely based around the Turing Machine model. Lambda calculus is an effective lens to design programming languages and prove equivalence between programs. We know by way of the Church-Turing Thesis that these two models are equivalent. The Turing Machine model is both better studied from a computation perspective and has much more practical realization; what's the point in creating something like this? It feels a bit like silly lambda calculus fetishism, but again maybe the value here is the actual computation formalism itself.

[cybernautique]

For me, personally, I really like the lambda calculus as a tool to organize and better my computational thinking.

I came into programming/computer science from a mathematics degree; I read some old treatises on recursion theory[1] and fell in love. I couldn't ever quite wrap my head around the Turing Machine formalism, but kept at it for a while. Finding Barendregt's paper [2] was a huge shock! I grasped it much quicker. So, yes, lambda calculus and the Turing Machine formalism are equivalent in explanatory power, but there are also reasons someone might prefer one to the other. So, yes, for me, the value _is_ the formalism.

As to why I think the Rekursiv would provide a good platform for implementing lambda calculus on the bare-metal, that's entirely due to Rekursiv's memory model advantage and the fact that it has a user-writable ISA. Why would someone choose to implement the lambda calculus on bare-metal? You call it "fetishism," I call it fun!

More generally, I just really like the idea of having a machine with a user-writable ISA.

[1] Theory of Recursive Functions and Effective Computability: https://openlibrary.org/books/OL2738948M/Theory_of_recursive...

[2] Introduction to Lambda Calculus: https://www.cse.chalmers.se/research/group/logic/TypesSS05/E...

[Karrot_Kream]

FWIW Nothing wrong with having fun with computing, and implementing lambda calculus on bare-metal can be as fun as any other computational exploration, so good on ya!

Thanks for clearing up that it's the formalism you find interesting. Also, to offer a counterpoint, I'm also from a math background, but I was more of an analysis person (as much as one can be in mathematics where it's all related) than an algebra person, and when I did some FP research, it often felt like where all the algebraists go to play computer science. I feel like analysts are underrepresented in PLT (and overrepresented in complexity theory!) but this is already going off-topic, so cheers.

[cybernautique]

Nah mate, s'all good! It's great to hear your feedback; I am very much of the algebraist spirit myself (I barely passed my Rudin-based real analysis course). Our experiences definitely align. FP feels much more like my favorite parts of math.

Out of curiosity, can you identify any areas in PLT that could be made more analyst-friendly?

Intuitively, it feels that PLT is almost necessarily of the algebraist; to me, one of the big divides is the discreteness of algebra vs the continuity of analysis. Would it help if there was a PLT that exhibited a greater degree of continuousness? If so, what do you think that might look like?

[Karrot_Kream]

Your comment made me think a lot! Thanks for that. If I had to "capture" what made analysis interesting for me, it's not just the notion of continuity, but the idea that we're analyzing the behavior of an object in the concrete instead of the abstract. That means taking an object and deriving all sorts of behaviors, instead of building up algebras from simple group/ring operations. To bring this back into PLT, it would probably mean the ability to place computational complexity bounds on functions/methods. Something like Mercury's Execution Modes https://www.mercurylang.org/information/doc-latest/mercury_r...

[cybernautique]

Very cool! I'd never seen this formalized, but it definitely has the color of some "hacks" I put together in Python (specifically the idea of "destructively updating" an item in an index, as opposed to appending an element to the end).

That's also a very interesting perspective on analysis. To get a better feel: is your joy of analysis in getting into the "internals" of an algebra, to directly derive properties of elements within the algebra as opposed to relying solely on global properties endemic to the construction of the algebra?