Comment by solomonb

What a wonderful response :)

> 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.