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...
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.
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?
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?
I'd also love to see your talk! Do you think a RISC Rekursiv could be achieved? What value, if any, do you think such might have in our current world?
http://www.wolczko.com/mushroom/
The slides for my 2019 talk about Smalltalk computers (in LibreOffice and PDF formats):
http://www.merlintec.com/download/2019_slides_jecel_fast1v2....
http://www.merlintec.com/download/2019_slides_jecel_fast1v2....
and the video (1 hour and 13 minutes):
https://www.youtube.com/watch?v=tATpzsyC6OA
If you replace the Rekursiv's special microcode memory with a cache to allow microcode to live in main memory you will essentially have a RISC version of the machine. I have adopted this solution in several of my own designs.
I'm also deeply in love with the merlintec website. It's refreshing to see a website which has persisted since 1999(!), and without a lick of JavaScript it would seem!
Could I purchase a Merlin 6 or a Pegasus 2000?
Speaking of which, the way that the Pegasus 2000's eGUI documentation[1] is written is incredibly dear. The "world" and "heaven" analogies are great!
If I may ask, from your perspective, what's more elegant about Rekursiv's design? Is it the philosophy or implementation? I'd also love any links to orthogonal persistence!
The Rekursiv advantage is its ability to do recursion on the bare-metal. It's described as an object-oriented architecture. Its memory was a persistent store of objects, with each object having its size, type, and position known in memory.
[1] https://en.wikipedia.org/wiki/Rekursiv