With AI tools, I remained on the fence/skeptical until Dec 2025. There has been a genuine technological revolution since then. I wouldn't tell other profs what they should do. But I think it would be hopelessly irresponsible of me, given *my* areas of speciality, to not know or care.
@shriramk Could you describe the nature of that technological revolution? What has fundamentally changed?
@sandorspruit Genuine question: have you tried using it?
@shriramk @sandorspruit I genuinely don't think that there is a relationship between not willing to hear, read or share about AI and understanding what AI can do.
@dimitriselectif @shriramk I just asked a question aimed at understanding deeply what AI can do, which implies I expressly want to hear about it?
@sandorspruit @dimitriselectif @shriramk
I'll try answering. As I understand it the first generation of these tools were not much more than the LLM. More recent versions of these tools - for programming at least - are augmented in a variety of ways. e.g. as of July Claude reportedly has Racket available*, meaning it could use the facilities of the Racket compiler and REPL.
The next bit I may be wrong about but I believe the modern services doing proofs have proof assistants, SAT solvers and other magic that I don't (yet) understand.
If I've got this wrong please tell me - I'm just trying to keep up like everyone else.
(*Sadly v8.10 - a year old but happens to be what was in the Debian package repo.)
I'm guessing
@spdegabrielle @dimitriselectif @shriramk Interesting, thanks! So then the direction is to use LLM + symbolic tools, which is kind of what you expect. Similar to meta tools like the use of compiler generators and that MPS-tool from Jetbrains.
@spdegabrielle @sandorspruit @dimitriselectif
You are correct.
It's not so much that the "services" have proof assistants — I don't know that Lean runs on Anthropic's servers — but rather that they output code for those assistants. It's no different from outputting *typed* code and letting your local, deterministic type-checker run over it and check the code. Except on steroids.
@shriramk @sandorspruit @dimitriselectif
So much to learn!
There is still much to worry about,
I don’t think these have been addressed.
Can I call these concerns ‘equity, environment and ethics’?
I forgot two
Sorry for the brain dump. I’m not asking for answers. I just had to get it out.
@spdegabrielle @sandorspruit @dimitriselectif
Yes to all. There's been plenty of talk about all of this.
I'm curious: have you tried running DrRacket with any non-trivial programs on the geriatric PCs in the public library? How well does it run? Does it even load?
Creating models is a 1-time activity. Using is far less intensive. Heck, you can just run an open-weight model on your laptop and see the energy usage for yourself.
@shriramk
It’s not a question I’ve been able to check for years because public libraries will not let you install software. (I bet Pyret works but I’ve not tried recently)
@spdegabrielle So that seems to already be something that I can do with commercial AI that I can't with Racket. (-:
Pyret will start up reasonably (depending on the thickness of your network pipe), but large tasks may exhaust the machine.
I was in Cambridge the week the Raspberry Pi came out. They were SO excited to show it to me as revolutionary for education. They had a keyboard and monitor. I entered wescheme.org . A few minutes later…they said "well, maybe it's not ready for that yet".
@shriramk @spdegabrielle @sandorspruit @dimitriselectif
I am not a programmer, but I would like to understand better the epistemic aspects of automatic code verification.
If your code is generated by an LLM, then translated to LEAN also by an LLM, what does the correctness of the LEAN proof tell you?
@nicoformanek
It depends on who wrote the spec/how the spec was obtained. (For "spec" here you can substitute "theorem statement".)
If the spec is "correct", and if you trust Lean (which is independent of AI), then you have great reason to trust the code.
Of course, if you just vibe the spec too, then you're asking for trouble. That's why I'm focusing on that part in my research:
https://blog.brownplt.org/2026/06/09/pick.html
@spdegabrielle @sandorspruit @dimitriselectif
@shriramk @nicoformanek @spdegabrielle @dimitriselectif But writing the spec can be more difficult than writing the code?
@sandorspruit
The problem is we're living in a world (of GenAI coding) where everyone IS writing specs. They're writing descriptions of what they want, and leaving most/all the implementation details to the GenAI — exactly what a spec is. So it turns out people *do* want to write specs — but are totally untrained to do it well. Hence my shift in focus.
@nicoformanek @spdegabrielle @dimitriselectif
Sep 24, 2026, 10:02 AM@shriramk @sandorspruit @nicoformanek @spdegabrielle @dimitriselectif that's an interesting way of putting it; and I have to agree with Sandor, with a caveat: writing a GOOD spec can be quite difficult
@dif @shriramk @nicoformanek @spdegabrielle @dimitriselectif A poor spec is no spec at all 😁😎
Sep 24, 2026, 11:07 AM@sandorspruit @shriramk @nicoformanek @spdegabrielle @dimitriselectif i don't know, for many things it is kind of okay to have a poor spec, and if you are in an LLM "loop" you are always refining the spec as you go
(of course a good spec is better than a bad spec; hard to argue otherwise!)
@dif @sandorspruit @nicoformanek @spdegabrielle @dimitriselectif
Yes, exactly. People do this all the time. It's just that the iteration loop has gotten a lot shorter.
If you were in a waterfall model hiring an external consultant, you wrote a spec and spent a million and waited a year and then said "Oh, that's not quite right". Now you can have that iteration in an hour w/ an AI.
We have NEVER had perfect specs and it is not meaningful to expect that of humans. ↵
@dif @sandorspruit @nicoformanek @spdegabrielle @dimitriselectif
In our "Decomposing Verification Around End-User Features" paper (https://cs.brown.edu/people/sk/Publications/Papers/Published/fk-decomp-verif-features/) I included this figure, inspired by something I'd heard Michael Jackson (the software engineer) say. You distill from the world into a spec, then you write code; the code now becomes part of the world, and thereby often itself alters the spec. Just the act of seeing what you asked for realized makes you realize all kinds of things. ↵
@dif @sandorspruit @nicoformanek @spdegabrielle @dimitriselectif
When you live in a high-friction world, you really, really need to get the spec as right as possible, no matter how humanly difficult that is. When that friction reduces massively, you can write specs far more incrementally.
This is not new. When we had only batch programming, we programmed in fundamentally different ways than once we got interaction, REPLs, etc. ↵
@dif @sandorspruit @nicoformanek @spdegabrielle @dimitriselectif
To be clear: I am NOT saying that removing friction is good. It can be very bad! I grew up in the "batch" model, so I also know the upsides to thinking carefully over hacking away. I've often fantasized about adding an exponential backoff to the "Run" button in Pyret/Racket. Run too often and it says "chill, buddy, think harder". ↵
@dif @sandorspruit @nicoformanek @spdegabrielle @dimitriselectif
Likewise, with GenAI coding, if you over-commit to code up front, you have *already* created technical debt, in the first hour of a project! But something that has gotten really good with top-end models is planning modes. I write my spec, then I have it poke at it, then we go into an extensive planning phase. I ask it to ask me all the questions it can think of; even my "good spec" can inspire 15-20 follow-ups. No code early. ↵
@dif @sandorspruit @nicoformanek @spdegabrielle @dimitriselectif
This is a model that works especially well, and what I'm also teaching to my students. We do high-level planning, then we go over all the data structuring (eg, what tables, what indices, what cross-references, why aren't those two tables one, why isn't this table two, etc.), types in the code, intended key function signatures, etc., etc. Planning doc iteratively improved to 20-30 items. THEN you "let it cook". ↵
@dif @sandorspruit @nicoformanek @spdegabrielle @dimitriselectif
So the same GenAI that can lead to slop code can actually lead to *really good specs*. And as a result, much higher-quality software. Certainly a combination of me, a planning document, the agent's memory, and a checklist/todo list can accomplish orders of magnitude more than I can alone, while producing much richer and maybe even (*shudder*) higher-quality software than me alone. ↵
@shriramk
Thanks, that helped a lot. If we bracket the skepticism towards LEAN (which might or might not become a problem in the future), my understanding is now that in software engineering you will have high trust in any means towards an end, if the end is specified well and you have an independent piece of software which certifies that said means will achieve said end.
This differs a lot from mathematical proofs, which are an end in themselves. And people are really at loss what to do with 13M lines of autoformalized LEAN code.
@dimitriselectif @sandorspruit
You're doing the exact thing that makes this platform sometimes look unhinged.
@shriramk @sandorspruit Attacking someone for giving its own opinion that doesn't go in the desired direction is unhinged, you're right about that.
Oct 1, 2026, 5:53 PM@shriramk I can't speak for @sandorspruit, professor, but I have tried using LLM sludge (I remind you that it's practically impossible to avoid these days because Google and Microsoft etc. are forcibly shoving LLM trash down the gullets of their users) and thus I know from experience that LLMs are worthless except as brute-force instruments in the hands of the sort of people who probably shouldn't be trusted with professional decisions: the willingness to delegate decisions to a stochastic trash machine is a pretty damning trait in someone who ought to care more about making well-considered choices rather than leaving them in the hands of stochastically assembled garbage.
Do you incorporate LLM garbage into teaching materials, professor?
Oct 1, 2026, 5:58 PM@shriramk I also have to ask myself, professor, why those who have become addicted to being flattered by an LLM crap-factory—that seems to be the chief attractant at work, the fact that LLM sludge mimics human flattery and thus gives addicts a sweet little dose of insincere praise with every text output—refuse to acknowledge just how destructive and patently malevolent are the obvious corporate (and political) goals behind the #technology sector push to force LLM sludge into general use, whether or not it's desired by anyone more than a thin stratum of elitists.
Elitists such as yourself, professor.
@mxchara Hi. A few things.
1. Maybe you think that by insulting me as hard as you can, you'll either (a) convince me of something or (b) get a rise out of me. Sadly, neither is happening or is likely to happen.
2. I gladly discuss things at great length with my students, their parents, my fellow professors, our alumni, and my professional colleagues. If you are one of those, reach out through appropriate channels.
3. Don't assume you know someone else's position from 2-3 sentences.
Bye. 👋
Oct 1, 2026, 11:41 PM@shriramk I wasn't insulting you! I was casting doubt upon your ethics. That's not an insult; there's no reason I should expect ethical behavior from a typical computer teacher. It's not in the nature of your profession.
Oct 1, 2026, 6:48 PM@sandorspruit Ah, that's too bad. You should care more about how @shriramk is betraying education and students, and fear less for "tone".
Oct 1, 2026, 6:49 PMIt comes down to this, @sandorspruit. It's not actually possible to speak nicely about technofascism and its manifestations.
@mxchara @shriramk Not every application of AI or even LLM’s immediately qualifies as a manifestation of techno-fascism, as you call it. The field already exists for decades.
The intent behind my original question was to stay away from discussions about Bigtech/AI, on which I suspect we largely agree, and focus on smaller and more interesting off the radar developments.
@sandorspruit
I should note that thanks to all the yelling and screaming, we have never gotten to your original question. And as this "conversation" tree has demonstrated, it seems quite impossible to do so on Mastodon, unfortunately.
@mxchara
Oct 1, 2026, 11:42 PM@shriramk I humbly invite you to try the fascist echo chamber on Twitter then. It seems more apt for you
@mxchara Oh, I think I'll stay on here just to irritate the likes of you then, thanks.
Sep 22, 2026, 9:00 PM@sandorspruit @shriramk Program synthesis now works, even at large scale.
Sep 22, 2026, 9:32 PM@sandorspruit @shriramk do you mean "why are LLMs able to do this" or "why do I think this is true" or "why is this a revolution"?
@samth @shriramk The revolution bit is obvious. But humanity has spent the best part of the last 2000 years, wondering about some of the things that LLM’s suddenly claim to do. Not hundred years ago, Gödels theorems seemed to impose serious limitations on what symbolic reasoning could do. Now, all of a sudden, folks claim all of this has changed.
Asking “why” seems a legitimate question…
Sep 22, 2026, 9:54 PM@sandorspruit @shriramk I agree, "why does this all work" is an excellent question that I don't think we know the answers to. But I don't think we in PL are well placed to answer it, and we don't have to in order to take stock of the revolution.
@sandorspruit @samth
Agreed. I struggle to understand why a high-enough dimensional space is enough for a rather dumb algorithm to produce remarkable output. But I've been surprised by volume and dimensionality before (eg, Alexei Efros's work on computational photography). ↵
@sandorspruit @samth
The way I see it, we're where the mechanical sciences were in the 1700s: people are inventing gadgets without really understanding how they work (and sometimes —because of that— they blow up!).
We're starting to get to the 1800s (Dalton, Carnot, Maxwell), with foundational sciences cropping up to explain and guide.
Then we'll get to the 1900s, 2000s, and so on.
Except in this domain we'll speedrun that explanation and engineering cycle; it'll take a decade at most.
@sandorspruit @samth
Think about steam engines.
People like Newcomen and Watt performed observations, had intuitions, and did experiments, and make significant progress. They made tremendously useful engines, even if the science was poor and the engines well short of optimal.
It took ~50 years before before Carnot explained the idealized thermodynamic model, and people could improve the engines from first principles.
We can think of current GenAI systems as being Watt engines.
@sandorspruit @samth
The steam engines created an entire industrial revolution even before the science was established.
A tremendous amount of useful and effective math was done long before we understood the foundations and limits (with new insights every century: epsilon-delta, Galois theory, Gödel, etc.).
This seems to be the nature of things? When the tool become useful enough, theoreticians rush in to finally bring order.
@shriramk @sandorspruit @samth its not merely enough dimensionality to avoid local minima. its also… absolutely absurd levels of compute. so it is a combination of sufficiently fast chips with sufficient memory… and subsidization.
Sep 23, 2026, 1:36 AM@gershom @shriramk @sandorspruit I mean, I recognize all of that. But it's still a big pile of matrix multiplication that can solve famous math problems.
@shriramk @sandorspruit @samth i think lately of the “its all so stupid” speech from knives out 2: glass onion.
@sandorspruit @samth
There are certainly enough people on here who question how high that dimensionality is. (-:
@sandorspruit @samth
Most of my research these days is in applied cognitive science, actually.
@samth @sandorspruit
Yeah, that's a great starting point.
@shriramk @samth @sandorspruit The other thing is that many objectors think it is not programming, but have never used it!
That is the definition of ignorance. Not in the sense that means "dumb", but the one that means "don't know about it".
I can say that it is still the same game as in SICP or K&R, it just goes faster ...because I actually tried it.
If you just tell it "do stuff", you will have a shitty program.
@sayrer @shriramk @samth Many objectors have their objections on completely different grounds, that have little or nothing to do with code working or not. The projected energy use for some data centers, for example, is larger than the energy use of entire countries. If this pushes us over the edge on climate change tipping points, well, then your code no longer matters 😬
Also, while you experience “it is faster”, studies and observations actually measuring speed indicate the exact opposite. The nature of the work changes so drastically that it slows people down significantly. How you perceive all of this depends on your level of experience as well. TL;DR: there are dozens of angles on this.