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