Michael Clarkson teaches OCaml at Cornell. I highly recommend his free course materials [1]. He’s an excellent educator. Learning functional programming paradigms had a major influence on how I design programs. Clarkson also taught snippets from the Pragmatic Programmer, which was equally influential (as it has been for many many others) [2].
Back in February, I was talking with my PhD advisor about using Lean to formally verify automated optimization modeling outputs. It eventually turned into this paper [1]. It’s been truly incredible to see how much the frontier models have progressed in both autoformalization and automated theorem proving in the last six months. Back in February, it was cool to see them prove the validity of some simple cutting planes. Now it can churn out a min-cut max-flow duality formalization (not to mention FLT). Very exciting times!
I’ll also share a Python package I wrote for automated theorem proving that has been super useful in my own research [2].
I read The World-Ending Fire (Wendell Berry), Hackers (Steven Levy), and Zen and the Art of Motorcycle Maintenance (Robert Pirsig) around the same time. I was struck by how similar Berry, Pirsig, and the early MIT hackers thought about Quality work. I gave a talk about it at an images & algorithms class I took in undergrad. It's reassuring to see Wendell Berry was an influential figure to many others in this space. RIP.
I haven’t read Berry, but he just went up on my priority list based on this.
Another link to Quality in the Pirsig sense I haven’t seen discussed much is Christopher Alexander’s work. Specifically A Timeless Way of Building which gives similar frustratingly inexact descriptions.
I guess Jane Jacobs fits in with this as well but with a bit more concreteness.
Thanks for the recommendations. Horse-Drawn Tools and the Doctrine of Labor Saving is a very short Berry essay and particularly relevant to this conversation.
I’m not sure I’m quite ready to take on 3 books to figure this out - can you explain a little bit what you mean about quality work? Consider my interest piqued!
I'm afraid I won't do this justice, as it's been a while since I've thought deeply about these ideas, but here is an attempt!
For me, Pirsig put it best: "Quality is the goal of Art." I too struggled to understand Pirsig's full metaphysical hierarchy of Quality, but this quote gets at the core of the similarities I saw in these books.
Pirsig was concerned with teaching his students writing and maintaining his motorcycle. Berry was concerned with doing fulfilling and meaningful work on the farm. The MIT hackers were concerned with finding The Right Thing: "the unique, correct, elegant [program]." All of these individuals were concerned with some notion of Quality.
Interestingly, they all viewed what they were doing as a form of art. A colleague remarked, "Sounds like art," to Pirsig upon hearing his ideas on Quality, to which he responded, "Well, it is art." Levy identifies "You can create art and beauty on the computer." as one of the tenets of The Hacker Ethic. "[A]ll serious computer programs are expressions of an individual." This was the first clue to me that they were all talking about the same thing.
Like art, Quality is more a description of a process than product. And the Quality way of working that all three books discuss is very much the same. For me, it is exactly the defining characteristics of the artistic process. Through their work, an artist expresses themselves. They make contact with their medium, be that motorcycle, field, code, or painting. They make choices. Their medium responds. Both evolve with each other. The process is inherently experimental. Importantly, their medium imposes limitations and constraints.
I gave this talk back in 2024, two years after I took the course. At the time, I was frustrated with my lack of artistic output post-graduation. These readings made me realize my creative/artistic outlet had just changed for the time being. I took a lot of solace in that. Recently, I've been trying to understand how AI fits into my picture of Quality programming.
If you've come this far, you might be interested to see some of my image & algorithm work [1]. The decluttering, exaptation exhibition was the culmination of the class and an independent study.
I should also mention Shop Class as Soulcraft (Matthew B. Crawford) as another book that influenced my thinking.
This is great; I'm a big fan of Crawford (mainly The World Beyond Your Head) and you've re-piqued my interest in these slightly earlier authors.
It's also worth noting that all of this musing on art isn't surprising in a way; the ancient world all the up to medieval times didn't really such much distinction between the craftsman and the artist, a sharp distinction between "functional" and "aesthetic" is quite a modern sensibility. Everything old is new again!
Christopher Alexander, as mention elsewhere on this page, is also a great reference here. I'm working through his Nature of Order books at the moment, and although he can be long-winded and vague at times, I'm absolutely loving them.
Your comment made me think of a quote from the first book: "The view of order which I describe in this book is very different. It is even-handed with regard to ornament and function. Order is profoundly functional and profoundly ornamental."
I'm very bullish on proof automation as well. I'm currently researching AI for algorithm design and using automated theorem provers to get formal guarantees for generated algorithms.
To make a shameless plug, I'm working on a Python package called OpenATP [1] to make it easy to benchmark different models/harnesses for automated theorem proving. It supports running agents in Docker containers or Modal out of the box. If you try it out, I'd love to get your feedback!
I recently wrote about the surprisingly good performance I saw from Grok [2]. On more challenging proofs, Grok doesn't keep up with Opus/Fable and GPT 5.6. I was recently blown away by GPT 5.6 Sol. It's persistence in closing out proofs is unparalleled from what I've seen so far. OpenATP also supports Kimi and Leanstral [3], among others.
This is super cool! I see you are using Aristotle as the automated theorem prover. I know Aristotle is free (for now at least), and it's hard to beat free... But, you still might be interested in a recent post of mine [1]! I'm working on an open-source Python package called OpenATP [2] to make it easy to run/benchmark different models and harnesses as automated theorem provers. I recently added support for Grok 4.5 and found it to be surprisingly good.
If you're excited about the relationship of Lean4 to LLMs/AI (like I am), you might find my recent post interesting [1].
TL;DR: I'm using automated theorem provers within my research on AI for automated algorithm design. To make it easier to run/benchmark different models/harnesses, I created an open-source Python package called OpenATP [2]. I recently added support to use Grok 4.5 in the OpenCode harness as a prover and found it to be surprisingly competitive with Claude Code and Codex at a fraction the cost and wall-clock time.
Try out Leanstral 1.5 on the latest version of OpenATP! OpenATP is an open-source Python package and CLI for agentic automated theorem provers. It natively supports running provers locally in Docker or remotely in Modal sandboxes.
Earnest question: any recommendation to not come off this way in forums?
I created this tool for my own research and have found it really helpful to benchmark different automated theorem provers (my experience so far has been that Claude Code + Codex still out-perform Leanstral). My genuine aim is to share that usefulness with others, not self promote!
Self promotion is fine here typically, I’d say the main thing here is it sounds like a tv ad. Try X! And not in response to a question or stated problem.
Here’s a tip, imagine how you’d comment if this wasn’t your library but just one that you knew and used. Would you have commented at all? Would you explain why you’d use it, how, the direct and clear relevance to the article?
Take that and add in that it’s your library.
If you wouldn’t comment otherwise, you’re just advertising a thing where people are. If you would, you’re contributing to a conversation with something you built.
Oh and there’s lots of open source products that have most useful features paid saas or licensed, or it’s an oss library that only talks to a paid saas thing.
Edit - the other thing you can do is just call out the comment at the start as self promotion or a plug, I think your work is more directly relevant here and doesn’t need that but it’s another approach when it’s a bit more tangential. That’s better here than other communities.
I don't know why but sometime ago, HN started resembling reddit, and there seems to be just widespread fear/jealousy/cynicism towards anybody advertising their work or services even, I don't think there was anything wrong with your post, it was informative.
Probably the most annoying part about Reddit and HN and X (although it let you mute people) is the abundance of "expert" opinions from people who aren't experts at all. You just end up with a bunch of false signals that you shouldn't even be listening to.
all in all I say invest in spreading the words via other channels, maybe even X is better and even the right time zone (besides US working hours, I find European time the worst statistically for sharing your work).
You know, I was going to reply to the person who called out your comment as an "ad", because I visited the site and it's actually relevant to the topic under discussion (Leanstral). And not even selling anything.
My thought was: Good job, this is tasteful personable marketing for a product with genuine value. I wish more marketing were done this way. So I think it's totally fine to be talking about the cool thing you're working on. I for one found it interesting and added to the discussion.
This is how it's often done, but personally, I'd prefer if the information "With this comment I want to promote something I made" came first, so that people who aren't interested can skip it.
Your comment is helpful, useful, and relevant. Please keep going.
Just my 2c, but maybe your original post could’ve been written in a less promotional / less excited way. It looked a little like spam at _first_ glance.
Really? I get a 403 that I must enable Lab models on https://admin.mistral.ai/plateforme/privacy. When I try to do that, it gives "There was an error trying to update the Labs setting."
Do you have that Labs setting enabled? When I contacted support, they said "enabling Labs models isn't available for self-serve activation on standard individual accounts." Do you have a different type of account?
[1] https://www.cs.cornell.edu/courses/cs3110/2025sp/
[2] https://pragprog.com/titles/tpp20/the-pragmatic-programmer-2...