To Proof Maintenance & Beyond!

PL research is dead, the age of PL exploration is just beginning!
   programming_languages research perspectives

There was a recent thread on the TYPES mailing list with researchers speculating about the future of our field given the disruptive effects of AI tools on programming in general.

The opinions in the thread were a mix of thoughtful stances. Some were positive, but the majority opinion was overwhelmingly negative. It wouldn't be too far to say that some researchers feel that they are facing an existential crisis right now:

I observe anecdotally that many people in academia are feeling worse about their work in Fall 2026 than a year ago …. Lower morale and motivation, higher stress and anxiety levels, and corresponding risks to mental health. The impact is comparable to what happened during COVID.

I wanted to write this thread to present an alternative position. I think many junior researchers at the moment are watching this discussion right now, students reeling with the daunting task of charting their careers in this tumultuous time, and worrying why they should even bother entering PL given this climate, and I'd like to give a slightly more positive vision for them.

To be honest, as a researcher, I have never been more excited! The wells of research ideas have never been so plentiful, new problems are popping up daily, and I'm able to ask and answer questions so much more quickly than before.

The central premise that I want to put down in this article is that as a community, we need to shift away from the ego-driven defense of our work, as some kind of demonstration of "effort" or "intelligence", and shift to the true and more noble motivation that should have been underpinning us the whole time! To one of exploration!

Programming Languages are Dead. So? Who cares?

Let's dig into the fears of practicing researchers, and let me put down a few points:

  • Language models are exceedingly good at writing code.
  • As such, humans are increasingly not going to be writing code.

Given this, it's understandable that researchers might worry that maybe their research is becoming obsolete. Humans aren't going to be writing programs. So why care about programming languages at all? Humans aren't going to be writing them.

Okay? So what?

Programming languages research has saddled the bridge between theory and application since its inception. As PL researchers, we get to work on principled and elegant ideas. We don't need to compromise those ideas for the sake of our practicality, but at the same time the downstream results of our work do eventually boil down to practical applications.

But… actually? who cares about the applications? I mean we don't even like applications? If we did we'd be in software engineering. I've worked with software engineering researchers. and believe me. It is NOT pretty. Their systems are ad-hoc, hacky, wildly incomplete and barely functional. But they need to be like that. You can't settle for beauty and elegance if you want to build a static analysis capable of handling the entire Linux kernel.

The point I'm trying to get at is that the beautiful ideas of PL, the insights? the beauty? they're all still here. They're all still available and we're more than able to still explore and play around and have fun with them. Who the heck cares if anyone uses programming languages? Let me let you in on a little secret. The vast majority of programming languages have literally 0 users other than their developers.

Fuck the users. Fuck the applications. Let's do some fucking PL research! And now with LLMs, we can tackle bigger and crazier problems than have ever been done before!

The New Wild West of Programming Languages Exploration

So I've explained why LLMs and the change in demographics of programmers shouldn't affect your enthusiasm for PL research, the ideas, the beauty, the fun, it's all still there! but now I'd like to tell you why LLMs make me extremely excited for the future of PL research.

In short, I think we now have access to crazyyy smart tools that allow us to answer and test and validate research counterfactuals at a pace never seen before. This is crazy.

The past few months, I have been absolutely crazed. I run into new ideas daily.

A lot of presumptions we build upon have been completely upturned. There's a real wealth of assumptions that our software ecosystem is built upon that no longer hold, and by questioning each one of them, we get entirely novel and fun research ideas.

  • Ship your interpreters — LLMs are incredibly capable of handling and managing tedious and boring proofs, at a scale no human would ever have done themselves. If we point an LLM at a problem, they can totally verify programs to the binary level. By exploiting this capability I ran an experiment of automatically generating semantics for interpreted languages, by getting the LLM to generate a semantics, and then prove that it abstracts the behaviours of the concrete binary of the language itself. This idea would have been absolutely unthinkable a year ago, but today? today it's just a month of prompting.
  • AI-first Verified Tooling (in progress) – Verification and language tooling are built for and around the limitations of human users. Anecdotally, it seems like the strengths and weaknesses of LLMs, while similar, are not always the same as humans, so maybe it might be possible to adapt the interfaces of tools to make them more amenable to the jagged intelligence of agents, for example, by exposing more details about tooling internals, such as the instantiation graph of an SMT solver etc. We're running some experiments with Amazon to try improving the capabilities of LLMs in using such verification tools by exposing these details.
  • Developing semantics for new languages (in progress) – Colleagues at my work developed a new language for dynamical systems (dynestyx). They were not programming languages researchers but we helped them to build a really cool new language which unified a TON of work in their area. This language lacks a formal semantics, and this would be something I would be extremely qualified to help them set up, but I am not an expert in their domain, nor do we really have the time to sit down and slowly get me up to speed in their area. Instead, as a new form of collaboration, I have been experimenting using LLMs to automatically generate mechanised big step semantics for their language, validate it with testing, and then working with them to iterate this semantics to match their intent.

Alongside these applied domains, LLMs are extremely exciting for theoretical work too. Being able to automate the effort of proof writing makes it extremely easy to ask counterfactuals. What if I add this construct to my language? is it still strongly normalising? what if I change my type system like this? is it still sound? I am now able to iterate at a pace I have never been able to do before.

Sure, I think I do feel some loss at the lack of effort I need to put in to do all these amazing stuff. I used to take deep pride in my programming and development. I've singlehandedly built hundreds of thousands of lines of code projects in obscure and niche languages. I've toiled away at designing and proving properties of esoteric type systems. My code was a craft, and a craft I took deep pride in. But in some sense, that was more my ego than my intellectual curiousity. The ideas? the insights? the exploration? none of these strictly needed my expertise.

So Long and Happy Hacking you Budding PL Researchers!

Abandon your ego! Free your soul! Give in to the joys of exploration. Research has always been about exploration. Expanding the frontiers of human knowledge. This is the beauty of science, and this is what it means to be a scientist. Ask more questions. Investigate. Dive deep. You now have tools that can let you ask and search and delve into the depths of reality like nothing before. Exploit them. Enjoy them.

Let the era of programming languages exploration begin!

I believe we're entering a genuinely transformative moment for our field, and I'm really looking forward to the wild wacky future we're about to step foot into!