By all means, feel free to copy the UI of any of my UI experiments! Most of the things I write I license under a liberal license to make sure people know they can do that; Dercuano http://canonical.org/~kragen/dercuano is in the public domain, for example, and it might have some things in it that you enjoy.

I like Philip Guo's Python Tutor, and I used it a few weeks ago to show my girlfriend some algorithmic stuff, but (following Victor's Magic Ink) I think its mandatory interactivity is a significant drawback. To the extent that it's possible to visualize a program's behavior as a static image — perhaps a zoomable one — rather than an animation or a slideshow, I think doing so is an improvement. (In many cases it's adequate to just use a comic strip, as Victor did in his binary-search visualization in Inventing on Principle, or as you are doing with your V, but sometimes that involves too much compromise.) But Python Tutor is already tackling a very difficult visualization problem, and the static equivalent is an even harder visualization problem.

I enjoy Conal's work but I haven't read Compiling to Categories yet. I don't know much about category theory or Haskell, so I always struggle with his papers.

The particular Victor thing I was thinking about when I said "overwhelming battery of data points" was Up and Down the Ladder of Abstraction, but it also applies to, for example, the circuit example in Inventing on Principle.

I think Prolog CLP(FD) is less powerful than miniKANREN, except in the sense that you can of course implement miniKANREN in Prolog, but I'm no expert. I haven't seen an equivalent to Byrd's mindblowing quine-generation paper that uses Prolog instead of Scheme for either the implementation or the language being interpreted; I wonder if you could get some mileage out of that approach?

What you're describing about modeling traces of programs for a Turing-complete machine with a finite state machine is something I'd like to see explored more. Of course it's straightforward to produce a conservative NFA approximation of a more powerul automaton: whenever the automaton makes a decision based on information that's excluded from the NFA's state, the NFA makes a nondeterministic choice among the possible alternatives. So, given any possible mapping from the state of the more powerful automaton into some finite set of states, you can straightforwardly compute the NFA, and from that you can compute a DFA. Bjoern Hoehrmann's parselov takes such an approach to the problem of parsing context-free grammars, for example. (For better or worse, his favorite logic programming language is SQL.)

A difficulty I have with the programming-as-Kolmogorov-compression approach is that, at least in the case of Co-dfns, it didn't really speed up the process of creating the software; in fact, it slowed it down. It might speed up the process of understanding the software for other people, which is the major benefit in my view of the similar compression of algebraic notation for equations, but I haven't seen strong evidence of that, and I've seen weak evidence of the opposite — legions of programmers throwing up their hands at maintaining APL code, calling it unreadable, and flocking to alternatives as soon as they became available, such as VisiCalc, MATLAB, S, and Lisp, and their modern replacements such as Gnumeric, Octave, Numpy, TensorFlow, R, and Python. I guess I finally need to buckle down and learn an APL after 25 years of dithering.

It's possible that with better visualizations of examples, some of that perceived difficulty will evaporate.

Thank you for this wonderful conversation! Forgive me for not having responded earlier.