> I'm going to be thinking about that for a while.
This is a deep and fascinating world to get into. Enjoy!
> It led me to a kind of branching, graph-like manner of learning...
Yes! I love this experience. It takes a little owrk but you can even import the
1lab as a library and re-implement whatever fragment of it you are trying to learn. Working through a proof using a proof checker is an amazing experience and is actually really fun.
The real learning (about the thing you are proving but also about type theory, programming language design, abstraction, etc) occurs while interactive with the proof checker. They all come with really sophisticated tools for interacting with the compiler and the code, interactions that are rather unlike any other ide experience.
> An interactive textbook as a computational medium I feel has a lot more potential for usefulness and expression
I agree 100%. PLFA is a great example of something in that direction but I think we could go a lot further. I've fantasized forever about something like the illustrated primer from Neal Stephenson's The Diamond Age (https://en.wikipedia.org/wiki/The_Diamond_Age). I think that LLMs + dependently type languages could get you close to it.
Thanks for further recommendations. Programming Language Foundations in Agda. The Diamond Age by Neal Stephenson. I made a note to look into these.
Oh I see one of the authors of PLFA is Philip Wadler, whose name I recognize from Haskell and various papers on programming language theory. There's a Lean version of the book too. https://github.com/plfa/plfl
> Working through a proof using a proof checker .. They all come with really sophisticated tools for interacting with the compiler and the code
I have some prior experience developing a specialized code editor for a template language, and remember thinking at the time how much more potential there is for an advanced interface that supports the author, that deeply integrates with type information, documentation, examples, etc. Not just for writing programs and templates, but also for "rich text" and multimedia documents - for example, including music scores, diagrams, graphs.
Speaking of dependently typed languages (whose definition I admit I don't fully grasp yet), it reminds me of a paper I find fascinating and have read multiple times.
Again I lack the foundational concepts to really understand it to satisfaction. So I'm sure the resources you recommended will be useful on my learning journey.
> I'm going to be thinking about that for a while.
This is a deep and fascinating world to get into. Enjoy!
> It led me to a kind of branching, graph-like manner of learning...
Yes! I love this experience. It takes a little owrk but you can even import the 1lab as a library and re-implement whatever fragment of it you are trying to learn. Working through a proof using a proof checker is an amazing experience and is actually really fun.
The real learning (about the thing you are proving but also about type theory, programming language design, abstraction, etc) occurs while interactive with the proof checker. They all come with really sophisticated tools for interacting with the compiler and the code, interactions that are rather unlike any other ide experience.
If you wanted a place to get started I would highly recommend PLFA: https://plfa.github.io/
> An interactive textbook as a computational medium I feel has a lot more potential for usefulness and expression
I agree 100%. PLFA is a great example of something in that direction but I think we could go a lot further. I've fantasized forever about something like the illustrated primer from Neal Stephenson's The Diamond Age (https://en.wikipedia.org/wiki/The_Diamond_Age). I think that LLMs + dependently type languages could get you close to it.