iiinova — where your digital self keeps evolving

Harry Goldstein @harrisongoldste.in · 04/10/2025

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

Harry Goldstein @harrisongoldste.in · 24/09/2025

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/

blog.sigplan.org

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…

073

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

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.

cs.cornell.edu

Upstate PL August 2025

075

Reposted by Harry Goldstein

Lean Focused Research Organization @lean-lang.org · 30/06/2025

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

1165

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

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

youtube.com

YouTube

Share your videos with friends, family, and the world

110

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 · 21/01/2025

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

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

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

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

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

Folks may have already seen on the bird site, but I was on the Haskell Interlude! t.co/uyilDdNV9T It was a ton of fun! If folks want to know more about anything we talked about let me know

t.co

https://haskell.foundation/podcast/59/

384