> Now is the time to do that.

Sigh.

https://www.amazon.com/Essentials-Programming-Languages-MIT-...

> they have lambda defined as an axiom

"They" is me -- I wrote that article. And no, "they" do not have lambda defined as an axiom. There are no axioms in that article because there are no proofs. It's just a demonstration of how you can do math using lambda calculus, with pairs being built along the way (and ultimately abandoned in favor of Church numerals) along with an actual implementation of a serializer for lambdas called lc-expand. If you don't see how that refutes your claim that "If you have a list defined "al la lambda calculus" as a lambda term, you can't really write it down fully" I'm not going to try to explain it to you. You are apparently beyond my ability to help.

My interpreters course used this book, as well as 'the little schemer'. They follow a lot of conventions that I find really useful for software development (various intricacies of languages in active development tend to follow the same conventions of diagramming, labeling, notation, etc - all really important things to keep standard when reasoning about, teaching, and explaining programming languages!)

https://www.amazon.com/Essentials-Programming-Languages-MIT-...

https://github.com/mwand/eopl3

https://mitpress.mit.edu/books/little-schemer-fourth-edition

There's also this book that from my understanding, a lot of people consider fairly foundational / useful (own it, haven't read it)

https://mitpress.mit.edu/sites/default/files/sicp/index.html