Well, if we're just interested in teaching the practical implications of Rice's Theorem & friends, then TMs can be completely dispensed with. Instead, use any of the equivalent models that's closer to practical languages, as exemplified by Jones' Computability and Complexity

Turns out I'm not alone in this (e.g., found this textbook by Jim Hefferon which I might give it a try in the near future: hefferon.net/computation/). Also looking to try a more semantic treatment of simpler models, using applications from formal methods & verification

Sorry, I meant alternative instead of selective. Time to go back to OCaml…

I had a random thought (when reading the free generator paper) that the selective applicative interface with a ”f a * f b -> f (a*b)” API instead of the usual “<*>” roughly corresponds to typed context-free expressions minus fixpoint. Might explain the expressiveness vs understandability tradeoff…

The most enlightening explanation on subtyping I read was from Benjamin Pierce's PhD thesis. Paraphrased, subtyping is type-directed program synthesis (intersection types synthesize tuple projections, nat<int synthesizes coercions, function contra & covariance synthesize function composition)

wow this sounds super interesting. Looking forward to reading your paper when it comes out!

was even thinking about designing an automata theory course around this idea: regex is just like a simple imperative language with atomic print(), but with if's and while's conditions being non-deterministic. Then everything becomes "predicting what a program will print by abstracting it into regex"

UPDATE: I am going to offer some free online training this summer about how to create code playbacks and use them in a course. I'll show how I use code playbacks instead of textbooks and videos and share what my students think of them.

www.eventbrite.com/e/beyond-tex...

Thanks for your fast response! I'll shoot an email

Hi Prof. Friedler, I'm very interested in applying for this position, and have some questions about the application materials for which I'd really appreciate your input! However, Bluesky doesn't seem to allow me to DM you via its Chat. Would you prefer me to reach out via other channels instead?