When the Hard Part Stops Being Hard | Proofs and Intuitions
When the Hard Part Stops Being Hard | Proofs and Intuitions
A few days ago, a paper I co-authored, Tracking Borrows with Regular<br>Expressions, was<br>accepted to OOPSLA’26. It presents a new type system for Move, a Rust-style<br>smart contract language, built on a rather cute idea: using regular expressions<br>to capture heap reachability. I won’t go into the technical details here. What I want to<br>talk about instead is how the paper was made and how the publication culture in<br>programming language research has changed in the past five months.
For this paper, the part that usually consumes about 80-90% of the effort in a<br>programming language (PL) design paper, the mechanisation of its meta-theory and<br>the formal soundness proofs, was done by one person (me) in Lean, using a<br>frontier LLM, in about four weeks, end-to-end, at the scale of a production<br>compiler rather than a toy calculus. I wrote about that experiment in a blog<br>post back in March.1 Back then,<br>I’ve given a several talks on this effort and discussed it with a a couple of<br>dozen of prominent members of the PL research community. While I received a fair<br>share of curiosity and enthusiasm, many reactions at the time ranged from<br>skepticism (“the formalisation must not have been hard enough”) to outright<br>rejection (“this is not how PL theory should be done”).
I think those reactions say something about our publication culture. Unless<br>research embodies a visible amount of human effort, or even struggle, it is<br>unlikely to be taken seriously. We do love elegant ideas in PL, but we prefer<br>them wrapped in eight to ten person-months of labour: a large implementation,<br>extensive benchmarking, or machine-checked proofs pushed through by hand. That<br>wrapper is now gone. An experienced researcher with a good idea can turn it<br>into a competent PL publication in about a month.
We used to raise eyebrows at the AI/ML world, where a month-long sprint from an<br>idea to a solid NeurIPS submission is, as I am told, routine. That is now our<br>reality too. When I described my experiment to Martin<br>Rinard, an MIT professor who was visiting<br>NUS at the time, it took him roughly a month to fully formalise in Lean an<br>optimising compiler he was working on, write a<br>paper about it, and submit it to a<br>conference, having never touched Lean before.
I don’t think we have fully absorbed what this does to our field, but the<br>first effects are already visible. What was surprising in March 2026 became<br>common knowledge by July 2026: POPL submissions nearly doubled this year, from ~350<br>to 600. The unexpected part is that the fraction of outright AI-generated slop<br>among them is relatively small. Most are pieces of competent research, produced at ten<br>times the usual pace, with the tedium of proofs, implementations, and<br>evaluation now largely automated. Having more than two papers at a single<br>POPL, PLDI, OOPSLA, or ICFP used to signal a strong vision, a prolific group,<br>and a wide network of collaborators. Now the same amount of research can be<br>done by a single PhD graduate with good ideas. Therefore, I would not be<br>surprised if three or four single-author papers at a top PL venue becomes<br>unremarkable within a year or two.
Why only a year or two? Because the community will inevitably raise the bar,<br>once we realise that producing old-style papers (“look, I defined a toy calculus<br>and proved it confluent!”) with modern tools is not a good use of anyone’s time.<br>In an age when anyone can build a<br>CompCert or a seL4<br>microkernel from scratch in the proof assistant of their<br>choice, we will have to become more ambitious, and take on challenges we could<br>not have imagined a couple of years ago.
In case you’re curious, the Lean development is available at<br>https://github.com/ilyasergey/lean-move. ↩
Share:
Comments