I started with SML in the 1980's, implementing a core math algorithm (Grobner bases) used in my K&R C computer algebra system Macaulay. Then I got this idea there should be a related algorithm in a different problem domain (Hilbert bases) and I managed to convert my code in twenty minutes. It ran. This completely blew my mind, on par with switching from punched card Fortran to an APL terminal in the 1970's.
Everyone talks a good line about more powerful, expressive programming languages till they need to put in the work. Ten years effort to program like ten people the rest of your life? I'm 69 now, I can see how such an investment pays off.
I moved to OCaml. Studying their library source code is the best intro ever to functional programming, but I felt your "all the way" pull and switched to Haskell. (Monads make explicit what a C program is doing anyway. Explicit means the compiler can better help. What it comes down to is making programming feel like thinking about algebra. This is only an advantage if one is receptive to the experience.)
I'm about to commit to Lean 4 as "going all the way". Early in AI pair programming, I tested a dozen languages including these with a challenging parallel test project, and concluded that AI couldn't handle Lean 4. It keeps trying to write proofs, despite Lean's excellence as a general purpose programming language, better than Haskell. That would be like asking for help with Ruby, and AI assuming you want to write a web server.
I now pay $200 a month for Anthropic Max access to Claude Code Opus 4 (regularly hitting limits) having committed to Swift (C meets Ruby, again not just for macOS apps, same category error) so I could have first class access to macOS graphics for my 3-manifold topology research. Alas, you can only build so high a building with stone, I need the abstraction leverage of best-in-category functional languages.
It turns out that Opus 4 can program in Lean 4, which I find more beautiful than any of the dozens of languages I've tried over a lifetime. Even Scheme with parentheses removal done right, and with far more powerful abstractions.
Yes. I'm impressed with Idris 2. I love how it uses Chez Scheme, my favorite scheme implementation. I contributed for a bit to getting Idris installation working on Apple Silicon Macs based on Racket's port of Chez Scheme, only to learn that I was working with Idris instructions that hadn't been updated.
Lean 4 is a better supported effort, with traction among mathematicians because of the math formalization goal.
I have more reasons to want to learn Lean 4. Peel away their syntax, and Lean 4 proofs are the word problem for typed trees with recursion. I find the reliance of AI on artificial neurons as arbitrary as so many advanced life forms on Earth sharing the same paltry code base for eyes, a nose, a mouth, and GI tracts. Just as many physicists see life as inevitable, in a billion runs of our simulation I'm sure AI would arise based on many foundations. Our AI fakes recursion effectively using many layers, but staring at the elementary particles that make up Lean proofs one sees a reification of thought itself, with recursion a native feature. I have to believe this would make a stronger foundation for AI.
I don't get that same rush looking at Idris. Using Lean 4 for general purpose programming? It must be good training.
I need a version of this for Lean 4; perhaps I can adapt this code.
AI generally struggles with less popular languages, and particularly with Lean 4, which is an excellent general purpose programming language that happens to have a primary goal to be a proof assistant. This skew in the training corpus really confuses AI.
Claude Opus 4 does better. I've looked at ways to serve the Lean 4 documentation; this Zig project is a better model for me.
Nia (https://www.trynia.ai) should generalize these tools, but it appears to have a "code base" focus for now. The right approach, but too specific a "system prompt".
Maybe https://context7.com/leanprover/lean4 is what you're looking for? I am not familiar with Lean 4 but Context7 has been working well enough for me, working in a completely different field though.
LLMs have issues with zig, namely outdated docs. Then I found @jedisct1's project, context7 MCPwhich provides a way to search through zig docs using natural language: https://github.com/jedisct1/zig-for-mcp
But context7 returns semantically processed responses that often summarize or rephrase the information instead of quoting it. And that's why there is now zig-mcp which returns documentation in markdown format for stdlib and builtin functions
I'm in the midst of modernizing a 1994 K&R C 32-bit codebase to 64-bit C23, as a museum piece: the computer algebra system Macaulay that I coauthored, since replaced by Macaulay 2.
The horror!
On macOS my environment is Sublime Text as editor, iTerm as terminal. I open two full screen iTerm windows of four panes each, start Claude Code Opus 4 and type "just task" in each pane. CLAUDE.md tells the session to run this justfile command and follow the directions, which generally include instructions to continue by doing "just task" again. Each session may edit its <file>.c and <file>.h but not shared headers; if it has a problem with this I touch STOP in the task directory, the other sessions eventually are told to wait, and then the trouble child session can edit what it wants.
I'm sure in a few years AI will read and fix my 57 C file code base all at once, but for now this workflow has proved invaluable.
The irony? This is the dumbest parallel task manager imaginable yet it works. And our code base has a similar feel: The storage management is a set of fixed sized stacks that outperformed malloc() by 4x back in the day. Etc. Etc.
I learned this gift from my Dad. He devised the Bayer filter for digital photography back in 1974, it looks like ten minutes work (it wasn't) but we're still using it.
Out of curiosity, ~how many lines of C in all is the C you're refactoring?
Reason I ask is I have gotten outstanding results from gemini pro 2.5, which has a very large context.
It already accepts very large individual messages, however if the code base is still too big for a single message, it is possible to send it all in multiple messages and still have the model keep it all in context.
For large, system wide refactors, this can provide planning that claude code can't or won't do efficiently.
Sometimes, I'll have claude code come up with a plan, feed all the related code to gemini, and then provide claude code gemeni's improved plan.
Then after the work is done, have gemeni validate the implementation.
I've looked a bit into automation around this but haven't picked something yet.
If anyone has a solid workflow for this already, I'm all ears.
Yup. I'm on a side project trying to port the 1980's computer algebra system Macaulay I coauthored from 32-bit K&R C to 64-bit C23.
K&R C is underspecified. And anyone who whines about AI code quality? Hold my beer, look at our 1980's source.
I routinely have a task manager feed eight parallel Claude Code Opus 4 sessions their next source file to study for a specific purpose, to get through all 57 faster. That will hit my $200 Max limit, reliably.
Of course I should just wait a year, and AI will read the code base all at once. People _talk_ like it does now. It doesn't. Filtering information is THE critical issue for managing AI in 2025.
The most useful tool I've written to support this effort is a tmux interface, so AI and I can debug together two terminal sessions at once: The old 32-bit code running on a Linode instance, and the new 64-bit code running locally on macOS. I wasn't happy with how the tools for this worked, that I could find online. It blows my mind to watch Opus 4 debug.
I made the short bibliography of the original bitcoin paper because of Merkle trees. Damn, I wish I'd put $1,000 into bitcoins then; I'd be a billionaire. I thought bitcoin was a Ponzi scheme.
A pure mathematician far from CS, I nevertheless wondered about digital timestamps, and convinced myself they were impossible. Then I went to a talk by Stuart Haber, supported by a paper with funny quotes starting each section. He explained the purpose of an observer to make timestamps work, but they were using a linear linked list.
As a coauthor of the original Macaulay computer algebra system, with some low-level coding chops, it was obvious to me a tree would help here. And there had just been a NYTimes story about how the nascent internet was accelerating research in CS, people would be on vacation for a week and miss entire start-to-finish events.
I stayed up to dawn writing a polite parody of their paper, introducing the use of a tree, emailed it to everyone I recalled had been at the talk, and went to sleep. That's all I ever contributed; I ended up on the joint paper even though my contribution turned out to be a "Merkle tree".
It's not a Ponzi scheme, because those have a specific definition. But it does sort of look like one. And all of the "meme" coins seem to be actual, if incredibly short-lived Ponzi schemes.
Pyramid schemes, Ponzi schemes, MLMs, NFTs, Crypto, Memecoins... they're all greater fool scams. All based around playing "hot potato" with investments, where early adopters push the potato on later & greater fools.
Memecoins are the most fascinating type of it because with other schemes, there's usually some veneer of legitimacy (i.e. you gotta actually try to scam somebody). I imagine at this point everybody involved with memecoins understands they're scam, and they're essentially just gambling instead of getting scammed. Although, effectively, gambling is its own type of scam.
I think you add some stocks there too. Particularly meme stocks.
Many people "investing" in crypto don't understand that stocks/shares give you have extra value because they pay dividends and give you voting rights for the direction a company takes.
You were basically right about Bitcoin, but tragically mistaken about the wisdom of getting in on the ground floor of the biggest Ponzi(-ish) scheme in history.
tmux! That was today's project. I'm using Claude Code Opus 4 to translate a K&R C computer algebra system (Macaulay) from the 1980's into C23. Finally getting to the "compiles but crashes" (64 bit issues) I found us living inside the lldb debugger. While I vastly prefer a true terminal to the periscope AI agent view in Cursor, it was still painful having at best a partial view of Claude's shell use, interleaved with our chat. What I wanted was a separate terminal session AI and I could share as equal partners.
tmux is the quickest way to implement such an idea.
I jumped at this HN post, because Claude Code Opus 4 has this stupid habit of never terminating files with a return.
To test a new hook one needs to restart claude. Better to run the actual processing through a script one can continually edit in one session. This script uses formatters on C files and shell scripts, and just fixes missing returns on other files.
As usual claude and other AI is poor at breaking problems into small steps, and makes up ways to do things. The above hook receives a json file, which I first saved to disk, then extracted the file path and saved that to disk, then instead called save-hook.sh on that path. Now we're home after a couple of edits to save-hook.sh
This was all ten minutes. I wasted far more time letting it flail attempting bigger steps at once.
One can find opinions that Claude Code Opus 4 is worth the monthly $200 I pay for Anthropic's Max plan. Opus 4 is smarter; one either can't afford to use it, or can't afford not to use it. I'm in the latter group.
One feature others have noted is that the Opus 4 context buffer rarely "wears out" in a work session. It can, and one needs to recognize this and start over. With other agents, it was my routine experience that I'd be lucky to get an hour before having to restart my agent. A reliable way to induce this "cliff" is to let AI take on a much too hard problem in one step, then flail helplessly trying to fix their mess. Vibe-coding an unsuitable problem. One can even kill Opus 4 this way, but that's no way to run a race horse.
Some "persistence of memory" harness is as important as one's testing harness, for effective AI coding. With the right care having AI edit its own context prompts for orienting new sessions, this all matters less. AI is spectacularly bad at breaking problems into small steps without our guidance, and small steps done right can be different sessions. I'll regularly start new sessions when I have a hunch that this will get me better focus for the next step. So the cliff isn't so important. But Opus 4 is smarter in other ways.
Sometimes after it flails for a while, but I think it's on the right path, I'll rewind the context to just before it started trying to solve the problem (but keep the code changes). And I'll tell it "I got this other guy to attempt what we just talked about, but it still has some problems."
Snipping out the flailing in this way seems to help.
AI is the primary audience for our writing, and the primary reason to reconsider our choice of markup format. It's all about semantic compression: Typst source, markdown, and asciidoc are far more concise than LaTeX source.
I'm observing, not here to convince anyone. The last six months of my life have been turned upside down, trying to discover the right touch for working with AI on topological research and code. It's hard to find good advice. Like surfing, the hardest part is all these people on the beach whining how the waves are kind of rough.
AI can actually read SVG math diagrams better than most people. AI doesn't like reading LaTeX source any more than I do.
I get the journal argument, but really? Some thawed-out-of-a-glacier journal editors still insist on two column formats, as if anyone still prints to paper. I'm old enough to not care. I'm thinking of publishing my work as a silent animation, and only later reluctantly releasing my AI prompts in the form of Typst documentation for the code.
> AI is the primary audience for our writing, and the primary reason to reconsider our choice of markup format.
That's AI which must adapt, not humans. If AI can't adapt then it can't be considered intelligent.
> Some thawed-out-of-a-glacier journal editors still insist on two column formats, as if anyone still prints to paper.
Narrow text is easier to read because you don't have to travel kilometres with your eyes. I purposely shrink width of the browser when reading longer texts.
Printing is still not uncommon in professional scientific environments. When you actually have to read a paper, it turns out that actual paper is quite convenient.
I've been wondering about this a lot lately, specifically if there's a way to optimise my writing for AI to return specific elements when it's scraped/summarised (or whatever).
Everyone talks a good line about more powerful, expressive programming languages till they need to put in the work. Ten years effort to program like ten people the rest of your life? I'm 69 now, I can see how such an investment pays off.
I moved to OCaml. Studying their library source code is the best intro ever to functional programming, but I felt your "all the way" pull and switched to Haskell. (Monads make explicit what a C program is doing anyway. Explicit means the compiler can better help. What it comes down to is making programming feel like thinking about algebra. This is only an advantage if one is receptive to the experience.)
I'm about to commit to Lean 4 as "going all the way". Early in AI pair programming, I tested a dozen languages including these with a challenging parallel test project, and concluded that AI couldn't handle Lean 4. It keeps trying to write proofs, despite Lean's excellence as a general purpose programming language, better than Haskell. That would be like asking for help with Ruby, and AI assuming you want to write a web server.
I now pay $200 a month for Anthropic Max access to Claude Code Opus 4 (regularly hitting limits) having committed to Swift (C meets Ruby, again not just for macOS apps, same category error) so I could have first class access to macOS graphics for my 3-manifold topology research. Alas, you can only build so high a building with stone, I need the abstraction leverage of best-in-category functional languages.
It turns out that Opus 4 can program in Lean 4, which I find more beautiful than any of the dozens of languages I've tried over a lifetime. Even Scheme with parentheses removal done right, and with far more powerful abstractions.
reply