Michal Wallace on Narrative Programming: Why Learn J when LLMs Code?

Michal Wallace (tangentstorm) loves pedagogy, producing many instructional videos, mostly for J and recently for Decker. For his dream programming course, he made a Forth-ish VM b4 and a REBOL-array-style implish. To assist with courses, he’s made tanco courseware around test-driven development and minavo, an “audio-video outliner” (a modern jprez.) Among many other things, he ran a webhost and worked as a professional K programmer, interviewed on the ArrayCast.

Pedagogy

What inspired your programming pedagogy (on youtube etc.?) Though a K programmer, on a previous interview you said you’re not only focused on them. This is quite unique as exotic language enthusiasts tend to evangelize their particular paradigm.

I have a long-term vision of making a programming course where I start with b4 (my forth-like VM) (or even more conceptual things like what a bit is and how to think about them)… Then building up from b4 assembly to a little Lisp and/or forth, a Pascal-like language, and then implish. With a lot of graphics and games along the way.

I made a lot of J videos because I think J is neat and because very few other people could make them (simply because the community is so small) while lots of people can and do make Python or Rust videos. The new Decker series is pretty much for the same reasons, plus the extra fact that I wanted to teach my daughter something. (She’s already taking classes in Scratch and will start Python after that.)

I wish I didn’t have to use any particular language in a video and could just talk about ideas. I tend to imagine I’m making a video about math or programming and just happen to use J or Lil or (eventually) one of the languages on B4.

We have my daughter enrolled in various human-led tutoring programs over the internet. (programming, math, punjabi, englcatish).. We did the scratch (and soon Python) classes because that’s what was on offer. I’m working one on one with her on Decker, but it’s slow going, because she can’t even type. (So one of the next videos will be a typing tutor I made.)

I started working with K at 1010data, but eventually it was bought by Symphony AI. We still use K every day, but most of what I do is in Python or javascript making little widgets to plug into our system or write demos for our API (which I maintain). We also have our own language with xml syntax.

JS has improved considerably. Before LLMs, I was often using a little library I made to abbreviate the routine JS routines in the DOM (browser APIs) (see example towards the bottom) although I don’t use this style at work.

The AI in “Symphony AI” predates LLMs. They were more focused on machine learning and data analytics before, but now I write tools for them in Python. Currently I’m working on an MCP server to expose the 1010 platform as a toolkit that the LLMs can use directly. He no longer works with 1010 data

How would you compare the different array languages you use? You worked with k, but mostly streamed j stuff. Do you find Lil lacks anything?

I miss forks and hooks when I use K, but I think overall I know most or all of K, because it’s very small. J has way more stuff, but I’ve constantly got the NuVoc (vocabulary website) open. (With K a 1-page printout covers it) I often find myself missing scan and insert in lil, but it winds up not being a big deal because explicit each loops are also very short. In Decker, I mostly miss talking to the outside world. (But the “danger zone” addresses that…) At the end of the day, I don’t really have strong preferences about implementation languages.

I don’t know why I don’t use K outside of work. Usually when I write code outside work, I’m either working on something that I want to eventually be a commercial product, or I’m thinking about how I could tell the story of the thing as a video. It stuck in my head that my channel was going to be a “J channel” and I should just stay on topic to build my brand and appease the youtube algorithm, but I guess I’m over that now.

When I make a video, I want to be able to say “and here’s how you can go try this for yourself.” Which is why I’ve never made a video about 1010’s system, even though it’s amazing. If there were a button where anyone could sign up for a free trial, I would have made those videos.

It’s only been relatively recently that there’s been any stable K systems that aren’t toys. (I livestreamed the video game I made in oK, but I never went back and edited or posted the videos).

I’m curious what you think of architecting big systems with these different programing paradigms.

Honestly, I think at a certain size they’re all pretty much the same. Even with 1010 or a cutting edge system like an LLM, there’s a few small parts that are really interesting and it really matters how you build it… And then the rest of it is all just connecting to other systems or generating HTML or moving files around. Important but you could probably write the same thing in COBOL or any language.

Different languages are good for different things, and in my ideal world (at least for personal programming / exploration / thinking with code), I’d have a bunch of small mini-languages that all shared the same runtime, so you could use whichever one you wanted. (This is lot like the racket philosophy, but in a much smaller, “fits in one person’s head” kind of approach.)

Forth

I find that big Forth programs are very hard to debug. I made a minesweeper in retroforth, and it has a bug in the floodfill routine that I’ve never been able to track down after numerous attempts over the years. Keeping things very small and using structured programming style helps a lot, but ideally I would bootstrap my way out of it.

I learned Forth by studying the ngaro virtual machine for retroforth 10. Retroforth is actually a mix of Forth and Joy (somewhat like Factor). Like Joy, it has a lot of quotations and combinators… And I found it much harder to learn that stuff than to understand the simple instruction set in the assembly language. On the other hand, there are a lot of things about the retroforth style that are much more modern than “standard” forth. (Like quotations…) The B4 assembler is very much inspired by my time with retroforth. To me a Forth is a system where you have 2 stacks and a dictionary of words, and the words are all about manipulating things on the stacks (especially the main stack). B4 has a bytecode , so in theory there are 256 operations, but the first 128 act as a 32-entry dictionary. You have 32 registers, each named with a single character, and each has 4 opcodes:

^A : call the routine whose address is in register A
@A : read register A onto the stack
!A : write top value on stack into register A
+A : add top value on stack to A, leaving old value of A in its place

Then there’s 32 opcodes that do arithmetic, stack manipulation (swap, dup), read and write arbitrary memory, jump, call/return… Very close to the same operations you find at the core of retroforth or John Earnest’s Mako or the GreenArrays chip. The other opcodes are mostly pluggable so other people can extend the system (I tend to make a single op for each host-language library I want to install.. Like there’s a terminal op that exposes terminal IO, etc…) Anyway, in the assembler, you have these core opcodes and there’s a few built-in macros for structured programming. (Like .i .e .t is an “if/else/then” macro).

I find that I’m able to write lots of cool things directly in the assembler… But usually when I write that way, I’m writing test-first and structuring it as a lesson plan / programming challenge. Here is pre (a parsing and regex system)’s test suite, which uses retro-style quotations (delimited with the .[ and .] macros) to define and use higher-order parser combinators directly in the assembly language. I built a very tiny Lisp with it. The goal is to blaze a trail for a student to later follow.

(The pre thing is a PEG system, like Rebol and Janet. I ported the concepts almost exactly from Alessandro Warth and Ian Piumatra’s OMeta paper.)

Each test suite is meant to be read and studied interactively, as a series of challenges to guide a student through building their own version of the thing, or at least understanding the existing version, via one of my other projects (named tanco with a prototype “course” at https://learntris.org/ ) All of that was to build up to the point that I don’t really care so much about Forth or even B4a as a language, but you have to start a beginner off somewhere, and B4 is meant to be a small and simple system that you can make yourself in a day or two (or just download one of the existing implementations) and then build your own toolkit.

Pascal

The plan I had was: establish the foundations with this tiny VM, then build a Pascal/oberon atop it (“retro Pascal”), using the Forth or Lisp (“b4th”/“b4s”) as scaffolding. And then eventually implish would be a high level blend of array languages and red/rebol/rye (which are nothing like racket but share that “make lots of dialects” philosophy)

REBOL! Rye! (I had not heard of Red.)

I’m not great at any of these languages. I’ve used Red a bit. I like that they’re all homoiconic like Lisp, but the syntax is much more flexible. Rye is a red-inspired language made in Go that has good support for tables as a native data type. It’s run by one person and seems to be really well done. Fixes a lot of things I don’t like about red, like removing weird stateful side-effects.

Free Pascal with Lazarus is an amazing tool. I don’t understand why people sleep on it. And Wirth…

Pascal pretty much died with windows 3.1… Microsoft and Apple both had Pascal compilers, but Turbo Pascal blew them out of the water. When windows came, Turbo Pascal became Delphi, and (afaik) way more expensive. I just can’t justify paying for a language like that… And then Delphi got handed from company to company, while Microsoft focused on C++ and visual basic and I guess apple did their own thing. So I think Pascal in general just didn’t have any companies left standing to promote it. (Even Niklaus Wirth moved on to Modula and eventually Oberon.)

I started using free Pascal to revive my old Turbo Pascal code. I didn’t really have anything of value. It was just sentimental. Then eventually I started using Lazarus for some things here and there. I don’t do a lot of GUI programming outside of a web browser, but when I do, Lazarus is definitely in my toolbox.

https://www.projectoberon.net/ is a huge inspiration for my work. One reason I wanted to model retro Pascal after Oberon is that I wanted to “play nice” with his Compiler Construction text… I don’t 100% know what that means in practice. I also just like Oberon. I found the uppercase keywords physically painful to type but I really like the way Oberon code looks, even without syntax highlighting.

I love Oberon, Alan Kay’s STEPS, Plan9… For the next few years, I’m focused on a table first language (k inspired but table first) with Prolog or such on top in a few hundred lines, to build a kOS thing a la duskos

I really admire these small systems like dusk/collapseOS as well, and in some sense I see B4 as my approach to that. I’m not concerned that civilization is going to collapse, but I do expect things to constantly change. 20 years from now, we might all be using Zig or Rust or Janet or your new table language, and I’ll be able to run my tools on top of that.

I think table-based languages are great. I have dreamed for years about making a “microsoft access for the web”, where you combine a RAD tool for building GUIs with a real database. 1010’s app building system isn’t drag-and drop like access, but our app-building system is similar in feel, in that you can wire together pre-built controls, and they all know how to talk to the database right out of the box.

John Earnest and I have a standing video call every couple weeks, and we often talk about Decker (I mostly contribute my abilities as a sounding board). A big part of the reason Decker is so constrained is to ensure it’s very hard to write software that rots. Like, (without the “danger zone” extension) your application can’t depend on external API or talk to JavaScript or even read an arbitrary file on your hard drive. I think the “danger” that the danger zone introduces is obsolescence. Elsewhere, I have code I no longer know how to compile, but so long as they get backed up somewhere, the decks I run today will be runnable by my great grandchildren. Unless of course I’m wrong and civilization DOES collapse… 😄

Webhosting

What was it like running a webhost?

Way back around 2000 or so, a friend and I were trying to start what we now call a SaaS. Basically our goal was to make something like what Shopify is today. We made a little shopping cart in PHP, and my friend brought in a few customers to subsidize development. But we knew nothing at all about running an online service, and so as a learning experiment, I rented a server from a data center, and emailed everyone I knew, asking if they’d like to host their website there.

Long story short, we never quite got the SaaS off the ground, but I ran the hosting company as a (mostly) one-person business for about 10 years. It paid my bills, but I never learned how to grow it, or turn it into a business that could survive without me. I treated it like a lifestyle business. In some sense, I was chained to my email, but I also had plenty of free time to follow my interests.

I spent a lot of time building things in Python with effort going into my control panel, billing system, admin scripts to manage the servers. This was long before there were successful web frameworks in Python, or companies like stripe that let you easily run credit cards, so I had to roll all that stuff myself.

I was one of the early bloggers, and so most of my customers were also bloggers. I even had a few months where I provided some bandwidth (which was expensive at the time) to blogger.com and they put a link to my hosting company right on the front page. I think that lasted up until google bought them.

When the 2008 financial crisis hit, I was still mostly just breaking even, and a decent percentage of my customers were in rough places financially, and decided they really didn’t need to spend money on their blogging hobby anymore. I started taking on more and more side work (even full time) to pay the bills, and that lead to my customer service getting pretty bad… and so more people left. It just kind of went into a downward spiral.

A big part of it was that I just wasn’t very focused. Several people had told me over the years that they thought I might have ADHD… And I thought (and still sort of think) that “ADHD” is a really ill-defined concept. There’s this book called the DSM that describes psychological conditions, and every time a new edition comes out, the rules about what ADHD are and how to diagnose it change. There’s no genetic test or anything. It’s like a checklist of behaviors. Anyway, my business going into a death spiral finally lead me to find a doctor that specialized in ADHD.

I still don’t necessarily believe in “ADHD” as a condition, but ADHD medication has absolutely changed my life. So much so that I feel like a very different person than the guy that ran that company. I still have one server that I use for myself, and I think there’s still a few sites hosted on it that probably haven’t changed in 15 years, but I don’t charge anyone money or deal with support anymore.

AI

How do you understand the importance of community? Do you expect e.g. more or less coding in array languages given the rise in LLM’s?

Henry Rich recently hosted a zoom meeting about using AI with J (I presented a bit about using the J-MCP server I made)… And one of the questions Henry asked was along the lines of… Why even do this? Why use J at all in the age of AI? I don’t know that I have an answer, but the question has been nagging at me.

I have this idea that there are two main problems in programming: Overchoice, and the Gestalt problem. Overchoice is a well-known concept in economics. It’s like how programming students get stressed out about what language to study. Or like even if it’s a much more narrow thing, like… We want to add a nice scrolling table to our database application. It’s going to run in the browser, so it has to be made with javascript… And then there are 50 choices and you have to pick one. At 1010 we once gave a junior developer the task of looking at a bunch of different viable scrolling table widgets and spending a week to integrate each one with our system… Just so we could pick one. Basically, small choices of technology turn into huge commitments, and then there’s a huge marketplace of available solutions, so we run into Overchoice just constantly.

But then it’s made much much worse by the harder problem… What I call the Gestalt Problem.

The Gestalt problem is just that to understand a system, you have to kind of load it into your head. Gestalt is a German word that means like the whole system, in the sense of the whole being greater than the sum of its parts. So you want to load an understanding of “the whole system” into your head, but your sensory channels are limited. You can really only hear one word at a time, in sequence. You can only see so many pixels in one image. Even if you have a huge 4k monitor with 5 source code files open at once, your eyes can only clearly focus on a small portion of the text at a time. So there’s just an inherent bottleneck in our anatomy that constrains how fast we can load things into our brain.

And with software systems, it’s worse than that, because they are interconnected graphs. They have this gestalt property. You can’t just open up the first source file in the directory, read it from top to bottom, and expect to understand the system. Decker’s source code is actually structured a bit like that. It’s multiple files but gets built into a single thing that you could in theory read from top to bottom, but even then, it’s just overwhelming.

So part of teaching a system is graph serialization… As a teacher who’s an expert in some system, you can try to make good choices about what parts of the graph to serialize first, so that the student starts building a model of the system with the most relevant parts first, rather than getting bogged down and frustrated with boring details that don’t matter.

(I screwed this up with the video I just posted. My daughter was bored to tears with the grid selector contraption. I spent all this time detailing a small thing that isn’t actually important for her understanding right now, because I want to use it in the next couple lessons. But I should have just introduced it as a new thing and moved onto those lessons.)

So! One thing that I really like about J is that you can compress a small amount of meaning into a few keypresses and get a big result on the screen. Once you have J (or K or whatever) you have a way to shrink the information that you have to send out of your brain through your hands (typing) and into your brain through your eyes. So these languages attack the constraint.

Tudor Girba helped me understand in a glamorous toolkit video “UI as a language” that GT has that same quality. It’s not necessarily Pharo/Smalltalk but the GT user interface itself. Instead of typing a few characters and getting a big result like in J, you can click a few buttons. This really stuck with me.

Decker and QuickApps (the 1010 system) have a mix of both. They both have these powerful array concepts on the coding side, plus this “RAD tool” like approach to the GUI where you can just stitch together a bunch of pre-made components and build something very quickly, sometimes without even needing code.

Where do LLMs fit into this?

LLMs do not experience the Gestalt problem!

I caused an LLM to write an MCP server for ngn/k. That codebase is written in the Arthur Whitney style. Code like that is probably a tiny tiny fraction of the LLM’s training set. Claude didn’t understand all of it. At one point I said: hey, stop trying to figure things out on your own. I’m a professional K developer. If you have questions, just ask. So it asked me some things, filled in its knowledge, and then within an hour we had working MCP tool for K. (And then later I went back and implemented K-IPC). I didn’t have to load the codebase into my head. It just worked.

AIs don’t solve the gestalt problem, because it’s still hard to load the understanding into your own head… But you can defer the problem indefinitely… Because why are you loading it into your head in the first place? Maybe it’s because you want to use the system. If you get hired as a Rust developer, you better learn everything you can about Rust. But maybe it’s because you’re dealing with overchoice… You’re trying to decide what tool to use, because you want to make sure it can do x, y, and z… And you just wished you knew enough about the system (or language or whatever) to have the confidence that you really could build the thing you want to eventually build after you’ve made the decision about the language or library or whatever.

Like. Maybe I’m just vaguely thinking about someday making a system in K. Which K? Maybe I think maybe this hypothetical K system might someday benefit from K-IPC. Like I don’t even know what the system is. It’s just the vaguest idea that I might build something someday.

This sounds dumb as I write it out, but it’s the fundamental feeling you get with overchoice:

If I spend my time learning K or Decker or J or anything, will I actually be able to do cool things with it, or will I have to constantly reinvent services that I get for free in other languages? Is it worth my time?

I don’t know what I need, but I see how useful K-IPC is at work, and so maybe when I’m looking at whether to adopt this K or that K (because there are many, and they’re not compatible), then maybe the presence or absence of K-IPC should factor into the decision of which one to focus on.

But ngn/k didn’t have K-ipc. oK doesn’t have it. Kona does have it, but maybe I observed kona crashed when I do this… Like if each of these tools came with an expert in that system, these issues wouldn’t matter, because the expert could just fix the crash or add the feature.

But I can’t do that without paying the Gestalt tax. So one option that’s exceedingly appealing to me or anyone in that situation is to make a new thing. And if I do that, and say I make it open source… Now I’m contributing to the overchoice problem and making it even worse for the next guy.

But the LLMs cut through all that. I added MCP and K-IPC to ngn/k in an evening each. When Eusebio announced Ksharp, I volunteered there and did the same thing. So the AIs aren’t experts in any of these systems, but because they have these massive context windows, they can just directly insert the entire gestalt (your source code) into their working memory, and so they instantly become - if not an expert - then at least knowledgeable enough to smooth things over for me.

I’ve always enjoyed using new languages and trying things out… In the far past, I’d read about a language (say Haskell) and play around a bit. I would do little throwaway projects like make a BDD library or implement learntris or B4vm in whatever language I wanted to play with. And then I’d go back to my main language, which was Python. (And then I’d get frustrated with Python for not having the neat features I saw in those other languages).

Then in the more recent past, I started just committing to doing a whole project in a language. So like… There’s a bunch of B4 implementations, but the Pascal one is the most fully fleshed out one with all the tools. (The intent being that eventually the tools run on b4 itself…) I have a bunch of implementations of BDDs. Bex started out as a BDD implementation in Rust just for fun, but I just kept at it and it’s the only one where I actually take it seriously and try to make it a real piece of software that people would actually use. The point is that these are all long term commitments, and you can only make so many of those.

How does this change how you pick a language for a project?

With LLMs, I feel like I can build a thing, and I never have to lock in to any particular choice, and I never have to worry if I’m making the wrong choice of platform, because I’m never locked in.

But you still eventually probably do want to commit to something, and you want to be able to transfer that understanding into your head. So at some point, after you’ve deferred as long as possible, you decide “yes, we’re on solid ground here, let’s really understand the system I’m building.” And that’s the point where you want a good language with that high compression rate.

Here is a file in bex. Bex represents boolean expressions as abstract syntax trees (ASTs), then converts them to canonical graphs like binary decision diagrams. Like a tiny thing like (A and B) becomes (if A then (if B then 1 else 0) else 0)… Only you draw it as a binary tree branching on A and then B. So here an AST with 2 nodes branched out into a tree with 5 nodes. But actually the two 0 nodes are shared, and even 0 and 1 point to the same node, with just a negation bit set on the edge. In most BDD systems, the 0 (or 1) node would be an actual object in memory and you’d have a pointer to it. But in bex, the pointer extends the idea of using a bit from the pointer as an inversion marker, and you can actually use 32 bits to store an entire truth table of 5 variables. (Plus a few more bits in the pointer can say which 5 variables). So actually in bex, for this example there’s no graph at all, just a single smart pointer that holds the entire truth table in its bits.

That’s the sort of thing it’s so easy to think about in J. And so all around the bex codebase, the Rust code has little comments with lines of J code. Because I use J as a language to talk ABOUT the system. I actually emailed Henry Rich about that Linear algebra textbook you mentioned in your ArrayCast… Because recently I watched Gilbert Strang’s Linear Algebra lessons from MIT… And the whole time I was using J to talk to AI to describe things I wanted to do. APL started out as a language and notation for humans to use to communicate with each other. And I think there’s an immense value in having these notations even for that purpose alone, regardless of whether or not anyone winds up writing software in it.

The followup about APL notation being a tool of thought/communication notation implies that there’s a community who practice this discipline and share the knowledge. It could be the case that you learn a style of communication with the machines… which you may generally only use one-on-one in your conversations with them, or when you use the repl.. but there’s still a community of practitioners. Like even I think Eric Iverson mentioned in his ArrayCast episode that the usual team size on a J project is 1 person… But there’s still room for a school around that discipline… The same way we have shared “schools” for martial arts.

The deaf community’s against cochlear implants because, if they solve deafness, no one would know sign language etc. and perpetuate their community. I used to think that was crazy. If e.g. J just becomes a way of talking to machines, how can there be a community around it? The recent spat of LLM-assisted array projects has been rubbing many array enthusiasts the wrong way. Many people don’t share code anymore, don’t make lessons.

I have a couple people around me who just absolutely hate the whole idea of AI and see it as clearly and obviously evil… And to me, it’s this life-changing, wonderful thing that is clearly, obviously, good. I mentioned John Earnest, who I consider one of my best friends, and he’s very anti-AI.

Mostly, I just don’t talk much about AI with him. For example, I did a game jam a few years ago ran into some bugs, most of which got fixed. In the end one blocked me from finishing the game, which has still not been fixed in the oK repo. But it is fixed in my copy, because an AI fixed it for me. And because of where it came from, that fix is never going to be merged.

Similarly, I have AI making little changes to Decker all the time. Like, I’m making these videos, so I want it to talk to my video making software. So like right now, I can have my script outline on the left of the screen and Decker on the right, and when I move around in the text of the outline, it changes to different cards in Decker. And in my browser, my Decker has a little button to save the deck over WebDAV (an HTTP extension for writing files back to a server) so I can just say “file->save” and it saves the most recent copy of the deck. (Whereas in normal web Decker, this would download it through your browser to your local file system).

There’s a part of me that thinks it would be really cool to make a hosted Decker service, where anyone could sign in and host their decks. I basically already have that. But I used AI to write it, and like even if John said it was okay to make that, it would just feel wrong based on his beliefs.

Like, I would feel okay with writing the whole webDAV backend manually, and then manually making those file-save changes to Decker without looking at what the AI did… But on the other hand, I’m just not going to do that.

There’s a discord server related to little forth-like languages, and I was invited to start a B4vm channel on it. And then one day, a lady was in that server basically calling for physical violence against anyone using AI. I confronted her about this. I did my best to be civil and polite, but of course I was annoyed. At some point I pointed out to the moderator that calling for physical violence goes against their posted rules. Anyway, the conversation with that person didn’t escalate or anything, but shortly after, the server added a new rule about not using AI. So, I shut down the channel and moved it to my own server.

(I’m not sure but I think there was also a rye channel on that same server, which was later forcefully removed because he used some AI to generate docs… But I wasn’t there for it.)

And then… I have a friend that I’ve known since high school that I’ve collaborated with on a few just-for-fun game projects. He’s a 3d artist, and he’s also very anti-AI, at least when it comes to game assets. He was on the fence about using it for coding, though… I showed him that you could just tell Claude what you wanted to make and it would make a version of the idea right there in your browser, even just as a prototype to show a hired dev later. He ultimately decided he wasn’t going to do that

Anyway, tying this all back to community, my point is that it’s not just that some people don’t like AI and some do… It’s like… This is a thing that’s going to really test some relationships.

If you fundamentally believe that what your friend is doing is evil, not just misguided, but actually evil and harming the world, how long do you stay friends with that person?

On the other hand… Say, you’re bouncing ideas back and forth and you hatch an idea together, if one person wants to use AI and the other refuses, one of those people is going to get there a whole lot faster. I imagine the Anti-AI folks thinking “yeah, good luck maintaining all that slop garbage code… Obviously the software craftsperson is going to win here.” I just don’t think that’s how it plays out in reality.

Is the idea that you are currently adding to the choice problem, but eventually will circle back with stuff to improve the core gestalt?

Ideally whenever you’re facing uncertainty, you want to leave your options open and defer making a commitment until you have the most information.

Adding to the overchoice problem (by going the “not invented here” route and rolling your own thing) feels like a tragedy of the commons thing. Making a new better thing is probably good in the long run, but it does add a small amount of cost.

I used to spend much of my day in a “learnprogramming” IRC channel and the choice of which language to learn was a serious stumbling block for people.We’d always say it really doesn’t matter. If you have someone around you who uses X, learn X. If you want to do web stuff, learn JS. Otherwise just start with Python. You could argue all day about whether that was a good answer, but it’s just a waste of time. The perception these new students have is if you go down this path, then you’re going to be a “Python guy” for the rest of your life, and that’s just not the case. The skills transfer.

But when you’re asking whether to build the project you’re going to base a business around, there really is lock-in, because now you have customers and you have to support it. If you change everything later, they’ll complain… Or you’re going to spend all your money hiring people to rebuild it and your company nearly goes under and you get sold.

Overchoice was always made worse by the gestalt problem, and vice versa, because they multiply each other. More choices mean more things you have to load into your brain just so you can compare them.

Anyway, the high cost of learning a system is due to graph serialization issues. The authors of a system generally start with a simple idea you could probably easily understand, but then keep growing it. But because they saw it evolve from the start, it remained understandable at each step.

I think you could make a system that fits in a single person’s head, and then also make it much easier to transfer to others if you told it as a story. My idea is a bit like literate programming, but instead of just writing a document that mixes code and text to describe the program as it is, you write a document that describes how it started, and how it evolved at each step… And at any point, you can extract the complete working system. I call that “narrative” programming, because it has that time component.

If you look at any of my videos, that’s exactly what I’m doing. For example, on these Decker videos, if you follow along in the decks, then each time you press “next” it copies the current state of everything you (the student) have done on the card over to the next card. So if you go back and flip through your deck, you can revisit exactly how it was built, step by step. A version control system gives you some of that, but the tools in jprez/minavo actually let you treat that whole narrative as a story.

And that’s the same reason the tests for B4 are designed to be read and worked through. That’s me leaving a trail for some future person to load that gestalt into their head.

Math

You use AI for math with Lean. What’s that like?

I am a college dropout, but I like to read math books and I really like formal proofs. I spent several weeks long ago attempting to formalize a proof of “Euler’s gem” (the polyhedron formula) in Isabelle. Eventually I gave up because it was taking way too much time, but I learned a lot. My first lean4 project was to write a prime number sieve. It took an hour or two to learn enough about lean to write the code, and then I spent the next six weeks defining what a prime number generator was.

I’m a huge fan of Practical Theory of Programming, Eric Hehner’s book/video course on formalizing programming. It takes a completely different approach than lean (which is all about type theory). It’s a much simpler, down to earth logic, and one of my goals for implish is to build it up from the basic logic he lays out in the book. The end goal is that you’ll be able to write formally verified programs in an APL-family language.

The AI+Lean stuff was more recent, and I’ve worked on two things:

First

There’s a site called Frontier Math that listed some problems that might be interesting to tackle with AI. I got interested in https://epoch.ai/frontiermath/open-problems/hadamard because it seemed at the time like the sort of thing a SAT solver could attack. The end goal is just to make a 668x668 array of signed bits (-1 or 1) that has certain properties. That’s a huge search space, but it turns out there’s a much smaller array of signed bits you can hunt for called a turyn-type sequence. That’s only (4*56)-1 bits (there’s one item missing in the bottom corner). Using Claude, I built a custom SAT solver in Rust, and between Claude, Codex, and Aristotle (another LLM that specializes in Lean) I formalized a handful of known results about Turyn sequences. Codex even came up with a new theorem about Turyn sequences that we eventually formalized. (It’s nothing earth shattering, but it wasn’t in the literature, and it should cut the search space down a little further. https://github.com/tangentstorm/turyn/blob/main/lean/Results.lean#L34 )

I didn’t find any new Turyn type sequences or Hadamard matrices, but I did formalize the entire chain of logic that explains how to go from one to the other.

The end result is still a huge search, but it’s the sort of thing that if someone spent enough money on compute, they could eventually find the thing. A large part of my effort was spent getting Claude to honestly calculate how long the complete, exhaustive search would take on given hardware. I don’t think I ever got a clear final answer (but think months or a small number of years, depending on how many machines you had running).

Second

Then I took on the “Jacobian Challenge”. This was something Kevin Buzzard posted on the Lean Zulip. He’s a math professor who has been one of the main people leading the charge for widescale formalization, especially in lean. This Jacobian challenge has nothing to do with the recent disproof of the “Jacobian Conjecture”, or about Jacobian Matrices, which is the main thing you’ll find on YouTube or google when you search for Jacobian, although all of these are named for the same mathematician. Rather, the “Jacobian” in question here has to do with topology. It’s basically an idea that Jacobi (and others) came up with in the 1800’s, and well-understood mathematics by those who study it. But the gap between what’s in Lean’s Mathlib and the statement of the Jacobian was pretty steep. Basically the task was to formalize everything in a small stack of math books.

I knew absolutely nothing about the topic, and tried for as long as I could to not learn anything about the topic, but rather just act as a project manager for the AIs. The scope of the problem was not clear to me at the start. Rather, we started with a Challenge file that Kevin hand-wrote. It’s got a handful of definitions, and around 20-something theorems, all filled in with the word “sorry” which is a lean word that means “just accept that this is true without proof”. And the goal is to make an equivalent file that has the same statements, but where every one of them is backed up with fully formalized proofs reaching all the way back to the axioms, preferably connecting up to things that already do exist in MathLib.

I went pretty hard on the Jacobian challenge. Kind of the reason for the challenge was that Kevin didn’t believe AI was capable of pulling the task off. And I wanted to show that not only was it capable, it didn’t need to be steered by an expert in the field. That’s why I tried my best not to learn anything.

I started with Aristotle, but by the end (this was a month or two) I had the max plans for Claude, Codex, and Gemini all working around the clock on this project. My approach was to just have the AIs pull the knowledge of what everything meant out of their own training, rather than trying to follow any particular textbook.

The bots and i basically wrote our own textbook (which of course I tried to avoid reading), in the form of a lean blueprint with “plain English” sections: https://tangentstorm.github.io/JacobianChallenge/blueprint/sect0001.html

Anyway, Claude Fable came out right at the end, and I got a massive boost in productivity. Then they shut Fable down, and I basically just stopped working, waiting for it to come back. Right around that same time, I found out another non-expert had used Fable to beat the challenge. He followed a textbook and also incorporated small parts of the other open-source attempts into the solution, including a tiny bit from mine, so at least I got to contribute to the “winning” entry in a small way.

A few months have passed, what’s up?

I got laid off at 1010. Since then, I’ve doubled down on minavo, adding video to the MVP and using it in a weekly livestream about AI tools.

I’ve finished an auto-formalization of the “Euler’s Gem” stuff I mentioned in lean, including a proof of Pick’s Theorem and the number of platonic solids. I also auto-formalized the Practical Theory of Programming book that I mentioned, and added an interpreter for his language, as well as a compiler to the lean version of b4: https://aptop.tangentcode.com/ I’m now convinced that auto-formalization is solved, and am hoping to turn my attention to auto-informalization: making tools to help humans make sense of formalized proofs.

Auto-informalization is very interesting. People dislike vibecoding for various reason, my biggest objection’s that they don’t increase understanding.

Yes, I think that’s one of John’s main concerns as well. For me, there are certain things where I care how it works, and other things where I care how it’s done. Very simple example: an early draft of the Pick’s theorem proof proved it by some method other than Euler’s polyhedron formula. But the whole point of the “Euler’s Gem” book (and my repository) is that Pick’s theorem is a direct consequence of the formula. So I made it go back and redo the work.

For Minavo, I care that every part of the system works, but there are only a few parts where I care how it works. For example, it has a plugin architecture, and you can extend it by writing little languages. So there’s a set of plugins that turn it into an authoring environment for J videos (animating and syntax highlighting the J repl), another for decker videos (flipping to particular cards in a deck), and a whole other set for making the animated chess puzzle videos at pawn takes world.

My hope is that there are certain kinds of animations that a particular creator wants to make, it’ll be easy for them (or their AI agent) to add plugins for them. And so I care very much about how that extension system works internally.

FWIW, now that Minavo’s coming along, I want to get back to making programming videos, where I care very deeply about every character and keystroke, and getting the viewer to understand what they’re seeing is the entire point of the video. I expect to use AI pretty heavily for those projects, but I don’t know what it’s going to look like yet. I have no problem putting my name on a video where I had even massive amounts of help making it, so long as it’s exactly the video I wanted to make (or better).

On the other hand, I’ll probably also explore building some specialized AI-generated channels. For example, I think it would be cool if we had a little channel with a short explainer for each J primitive. I think I’d be happy creating a template, giving the machine control of the text and visuals, and just giving it feedback on whatever it generates.