Harry Goldstein

I'll be at ICFP/SPLASH in Singapore, starting in a little over a week! Really looking forward to seeing everyone.

Think Globally, Discuss PL Locally In-person meetings are hugely beneficial for academic research; they provide a venue to collaborate and connect, making our community more connected and facilitating the exchange of ideas. In addit…

Have you been considering hosting a local PL meetup? Need a good place to start? Check out the PL Perspectives post that I wrote with Michael Greenberg and Noam Zilberstein!

blog.sigplan.org/2025/09/16/think-globally-discuss-pl-locally/

Upstate NY folks: Cornell will be hosting Upstate PL (www.cs.cornell.edu/upstate-pl/) on Thursday, August 28th. You should come if you're in the area!

Talk proposals are due August 4th, registration closes August 18th.

Really enjoyed this talk by @harrisongoldste.in that demonstrates inventive uses of the #LeanLang InfoView enhanced by metaprogramming techniques to display real-time testing data.

#LeanProver #Metaprogramming #VSCode #PropertyTesting

"That is actually a pitfall... when you rely on GitHub Copilot to provide the statement of your proof you actually have to check it gave… what you needed"

If one of the greatest math minds of our generation accepts incorrect AI generated code as correct, you will too
youtube.com/clip/Ugkx0fA...

Harrison Goldstein

If you are considering applying for a PhD this Fall, please get in touch. I’m looking for students who are interested in PL, SE, and/or HCI — and ideally all three! You can find more information about me and my work on my website: harrisongoldste.in

I'm incredibly excited to announce that I've accepted a tenure-track position as an assistant professor at the University at Buffalo!

The PL/SE group at UB is already really impressive, and I am honored to be part of its continued growth

Good thing Jane Street uses PBT for testing ;)

harrisongoldste.in/papers/icse2...

That’s fair. I think if you’d said “the PL community is under-reacting to AI” instead of “in denial” I probably wouldn’t have commented at all. But I guess that’s why this is your POPL *hot* take and not just a lukewarm take

All I’m trying to say is that PL approaches can solve problems in AI, without PL researchers actively working on AI. Because lots of problems in AI are the same problems we had before AI!

I think I now have too many responses to fit into 300 characters (or even a reasonable thread), but I agree with a lot of your points. I certainly want to make my work as relevant as possible to folks who are writing code with LLMs, and things I’m doing now are compatible with that goal

I don't think we disagree about the long game, I think you're just arguing that PL folks should bet on AI, and I'm saying that if they already have a different long-term bet that they're working on, there might not be a reason to pivot right now

What trends do you mean specifically?

I agree that there are also LLM-specific UX and SE questions that are important to explore, and I'd like to at some point. But there are also fundamental research directions in PBT that I think can improve software quality whether or not an LLM is in the loop

OP glossed over the fact that lots of non-AI work can still benefit AI. The goal of my testing research is to make it easier for programmers to thoroughly specify and test *any kind* of software. So programmers 100% can (and should!) use PBT to validate their LLM-generated code

I still have my Twitter account because I want to make sure folks can reach me for job market reasons, but I *cannot* wait to delete that account. The last few times I've logged in to check notifications I've seen videos of people getting injured on the main landing page? I don't need this

Why? I’m hoping to have a long career in research, so there’s no reason to move fast and break things. And I’m not saying wait 5 years to *think* about AI, I’m just saying I don’t know when in the next 5 years I’ll find a use-case that really feels worth pursuing seriously

I personally see places where AI might intersect my work over the next 5-10 years, but it'd be a big risk to drop everything and go after those projects right now. The technology is still evolving, and I have other projects in flight that I hope will be valuable regardless of where AI happens to go

It seems to me that PL folks in industry haven’t been shy about jumping into AI, and PL folks in academia have been slower to adopt because one of the benefits of academia is getting to play a longer game and waiting to see how new technologies develop. Isn’t that the system working?

Yeah, maybe. But a static guide is getting closer to the current state of things, where people self study from internet resources

Setting up assignments with good tests and build scripts is an easy win, yes. I’m disappointed more people don’t do that

Yes, agreed. It’s just not always clear when teach those tools. At the beginning of every class that needs C? That’d be like teaching Excel in every business class. Just the intro course? Someone could skip it.

I’m just adding nuance, I agree this is worth addressing, and we haven’t nailed it yet

I’ll play devil’s advocate and point out that the class is rarely actually “a class on C programming,” it’s a class on low-level computer systems. C is often the medium, not the goal. I agree students should be taught that stuff at some point, but it’s easy to see how it falls through the cracks

I feel a little bad about this, but at this point I think the only way to get remotely useful customer service from Xfinity (and maybe others) is to ask the AI bot to cancel your account. Within seconds it gives you a phone number for a human, and then those folks are usually very helpful!

I’m going to be at POPL next week, but only for two days (Wednesday and Thursday)! If you want to make sure we get a chance to chat, ping me here or via email so we can plan a time

Research Experiences for Undergraduates Are Necessary for an Equitable Research Community | Communications of the ACM Encouraging the expansion of undergraduate research programs.

Yeah, that is a shame. I think it’s an NSF issue, but I’m not sure

But yes, others should do this kind of thing too! @joshsunshine.bsky.social and Joey Velez-Ginorio wrote a great CACM article about why these kinds of programs are important dl.acm.org/doi/full/10....

REPL

Penn’s annual PL REU is accepting applications for Summer 2025! penn-repl.github.io

REPL is an awesome program. It’s fully funded (housing / travel / stipend) and you get to do research with an amazing group of people

Deadline is March 15th—if you’re an undergrad that likes PL, you should apply!

Thanks so much to JFP for publishing my dissertation abstract, along with 9 others!

This is a really valuable service for the community. Dissertations are a ton of work, and it’s nice to have a way to increase the chance that they’ll be read and used

Does anyone have advice around putting ongoing work in job talks? I have some exciting stuff in the pipeline that I'd love to share with folks, but it seems hard to do that without poisoning potential reviewers

Also, I know people talk about mechanized proofs as being like a video game, but I've been going back and forth between proofs and playing Pikmin 4 (great game), and they really do feel shockingly similar psychologically

Can someone do a psychological study on what Rocq/Lean proofs do to users' brains?

I've been doing some Lean proofs lately, and it focuses my attention in a way that almost nothing else does. And if I try to pull myself away in the middle, I find it very hard to context-switch