iiinova — where your digital self keeps evolving

Harry Goldstein @harrisongoldste.in · 07/05/2025

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

harrisongoldste.in

Harrison Goldstein

21810

Harry Goldstein @harrisongoldste.in · 07/05/2025

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

127410

Harry Goldstein @harrisongoldste.in · 12/02/2025

Good thing Jane Street uses PBT for testing ;) harrisongoldste.in/papers/icse2...

harrisongoldste.in

050

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

100

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!

000

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

100

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?

200

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

010

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

230

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

030

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

000

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

220

Harry Goldstein @harrisongoldste.in · 19/01/2025

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?

230

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

020

Harry Goldstein @harrisongoldste.in · 19/01/2025

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

100

Harry Goldstein @harrisongoldste.in · 19/01/2025

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

140

Harry Goldstein @harrisongoldste.in · 17/01/2025

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!

120

Harry Goldstein @harrisongoldste.in · 16/01/2025

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

080

Harry Goldstein @harrisongoldste.in · 15/01/2025

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....

dl.acm.org

Research Experiences for Undergraduates Are Necessary for an Equitable Research Community | Communications of the ACM

Encouraging the expansion of undergraduate research programs.

011

Harry Goldstein @harrisongoldste.in · 15/01/2025

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!

penn-repl.github.io

REPL

177

Harry Goldstein @harrisongoldste.in · 13/01/2025

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

1162

Harry Goldstein @harrisongoldste.in · 11/01/2025

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

030

Harry Goldstein @harrisongoldste.in · 05/01/2025

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

1142

Harry Goldstein @harrisongoldste.in · 05/01/2025

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

2284

Harry Goldstein @harrisongoldste.in · 31/12/2024

Thanks! I’ll check on it tomorrow and respond

000

Harry Goldstein @harrisongoldste.in · 26/12/2024

I agree with you in principle… but all I can say is I immediately knew what they meant by “inverted triangle,” even if that is technically meaningless

180

Harry Goldstein @harrisongoldste.in · 19/12/2024

It seems like they really make their money by making people the villains they sought to destroy

000

Harry Goldstein @harrisongoldste.in · 19/12/2024

I was just thinking this morning about how CLEAR’s violation of social contracts somehow feels like it crosses a line that PreCheck doesn’t

100

Harry Goldstein @harrisongoldste.in · 17/12/2024

I'm so glad you liked the interview! I'd be happy to chat more about applying recent PBT advances to hardware testing, if you're interested. I've kicked the idea around a bit before, but never with someone who really knows the hardware testing space

120

Yes, of course. And for those reading this who don't know we know each other, I'll say for the record that I know Mike has perfectly reasonable opinions about LLMs, and that I'm just giving him a hard time because that's what social media is for :)

010

OK, so they really are denying the existential then. That's a shame

000

OK, fair enough! I still think that until that point, you may continue to get push-back when you say an LLM can "solve <whatever>" when you mean it can "partially solve some instances of <whatever>." But I agree that once it surpasses human experts it makes sense to say "solve" unqualified

Harry Goldstein @harrisongoldste.in · 15/12/2024

IMO that’s exactly the issue. The original statement that “an LLM can solve <whatever>” has no baseline or point of comparison (even though it feels like it does, it’s up for interpretation). So a reasonable person could interpret it as “it can always solve <whatever> entirely correctly”

010

Put another way: are the people you’re talking to denying that *there exists* a FramaC spec that GPT can write? Because then I agree they’re just misinformed. But maybe they’re denying the *for all* statement

200

Harry Goldstein @harrisongoldste.in · 15/12/2024

Do you think these limitations around correctness, consistency, and scale will go away? Because if not then isn’t it moving the goalposts to say “it can do X kind of task,” when really it can only do Y instance, with errors, on a good day?

210

Harry Goldstein @harrisongoldste.in · 13/12/2024

I know I already posted about Lean once today, but I had to share: apparently new Lean projects automatically have CI set up?? github.com/leanprover/l... Amazing. I know it isn't hard to set up yourself, but I almost never use CI on personal projects because it's just a little too much of a hassle

github.com

GitHub - leanprover/lean-action: GitHub action for standard CI in Lean projects

GitHub action for standard CI in Lean projects. Contribute to leanprover/lean-action development by creating an account on GitHub.

020

Also, Lean's notations and the meta-programming infrastructure it's built on is incredibly powerful and advanced — if the Lean developers were paternalistically withholding power from users, I don't think they'd have bothered with all of that

000

My impression was that Agda implements a feature (simultaneous notation and data definition) that Lean does not implement. IMO choosing not to implement a feature that, at least according to OP, some users don't even want, is not making anything intentionally annoying

I agree that, taken too far, opinionated language design can have issues. But this isn’t about making something intentionally annoying — language designs have constraints, not everything can be equally easy. So it makes sense to choose the easy things based on the needs of your users

120

Harry Goldstein @harrisongoldste.in · 11/12/2024

Language designers always have to make tradeoffs between what’s going to be easy and what’s going to be hard. Why wouldn’t we use that tradeoff to make bad design choices hard and good design choices easy?

130

This is really cool! I’ll need to play around with it a bit. I think I skimmed the paper once a while back, but I never dug into the details. Thanks for reminding me about it!