@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. ↵
@dif @sandorspruit @nicoformanek @spdegabrielle @dimitriselectif
But please, let's not pretend that the average or even super-average programmer ever wrote great specs. Or, even more so, *maintained* them (one of the oldest and most persistent problems in SE). Once past textbook problems, specs are complicated, messy, contested, incomplete, inconsistent, and wrong. A good GenAI model will actually *help you find those issues*. If you have the patience to correct them, you get vastly better SE.
Sep 24, 2026, 11:59 AM@shriramk @sandorspruit @nicoformanek @spdegabrielle @dimitriselectif interesting to hear about your experience, and it does confirm what i have seen: the main component is still located between the keyboard and the chair
Sep 26, 2026, 7:24 PM@shriramk @dif @sandorspruit @nicoformanek @spdegabrielle @dimitriselectif I can see generative AI generating code for an underspecified spec ('I want a game'), but I am not convinced it will generate correct code for a full spec. I find it more likely that it'll hallucinate some best approximation. But I am ready to be proven otherwise.
@sprout @dif @sandorspruit @nicoformanek @spdegabrielle @dimitriselectif
Come on, it's 2026, are we still doing this?
Sep 26, 2026, 8:07 PM@shriramk @dif @sandorspruit @nicoformanek @spdegabrielle @dimitriselectif Sure we are, we need evidence. It's only 2026, and we're still in the early days of agentic AI. But I am ready to be surprised.
@sprout
Okay, feel free to believe that.
@dif @sandorspruit @nicoformanek @spdegabrielle @dimitriselectif
Sep 26, 2026, 11:11 PM@shriramk @dif @sandorspruit @nicoformanek @spdegabrielle @dimitriselectif Hey! I don't need your permission to believe anything? Anyway, we'll find out.
@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.