Laurence Tratt: Local Reasoning for Global Properties

Home

> Blog

Home> Blog

email<br>Bluesky<br>Mastodon<br>Twitter

Bluesky<br>Mastodon

Local Reasoning for Global Properties

RSS feed: whole site or just the blog

Recent posts

Local Reasoning for Global Properties

Test-case Reducers Are Underappreciated Debugging Tools

Retrofitting JIT Compilers into C Interpreters

PLISS 2026

Upcoming Talk in London

Async and Finaliser Deadlocks

What Context Can Bring to Terminal Mouse Clicks

Why Firsts Matter

LLM Inflation

Comparing the Glove80 and Maltron keyboards

Blog archive

In the last couple of years, I’ve increasingly been asked questions that boil<br>down to: will AI benefit from new kinds of programming languages? My answer has<br>been “probably not” and, so far at least, that answer has held up well: AI is now able to<br>generate large quantities of code in just about any programming language you or<br>I can think of.

Now that the technology has advanced, and its characteristics have started to<br>become clearer, my answer has changed. My experience is that AI – at least as<br>it stands right now – often generates high-quality local (e.g. a function)<br>chunks of code, but often struggles when asked to generate code that requires<br>a global understanding of the program. The easiest way to see this is a<br>proliferation of unnecessary defensive checks: these seem benign, but can cause<br>an exponential increase in the number of states later readers of the code believe<br>can occur, with all the deleterious effects that implies.

Perhaps this struggle will soon be overcome, but if it isn’t, we might once<br>again look to programming language design for help. My aim in this post isn’t<br>to try and predict the specific ways that programming languages will, or even<br>should, try to address this1. Instead I want to answer a more basic question: do<br>we have a good example of programming language design that allows local<br>reasoning to give us assurance about a surprising global property?

Background

I’ve made a fair chunk of my living out of programming languages, so I have<br>a vested interest in amplifying their importance. However, while I believe that<br>programming languages do have some influence on our productivity,<br>and on the reliability of the software we create, there isn’t much evidence that they<br>make a profound difference.

I don’t just mean “no-one’s been able to do a good experiment which proves<br>there are differences” — though that is true! Rather, a lot of “good”<br>software has been created in “bad” languages and a lot of “bad” software has<br>been created in “good” languages. It seems unlikely that the particular programming<br>language used was the main influence on such outcomes.

The simplest argument for this is that creating software that does everything its users<br>need, in a comprehensible and reliable way, requires empathy more<br>than it does expertise in challenging programming language features.<br>For a slightly more nuanced<br>view, I’ve previously tried to capture my thoughts on the nature of<br>software.

This shouldn’t be taken as me saying that programming languages don’t make any difference.<br>When I moved from programming in assembler to “high” level languages like Python and C, my<br>productivity increased substantially and I felt able to tackle much larger<br>pieces of software. The reason is simple: assembly forces me to deal with so<br>many low-level details that I continually forget the more important high-level<br>picture. The difference in the software I could create was profound.

Unfortunately, I gradually came to realise that such a huge improvement was<br>unlikely to be repeated. I had, slowly and ineptly, reinvented Fred Brooks’s no<br>silver bullet argument:

Most of the big past gains in software productivity have come from removing<br>artificial barriers that have made the accidental tasks inordinately hard,<br>such as severe hardware constraints, awkward programming languages, lack<br>of machine time. How much of what software engineers now do is still<br>devoted to the accidental, as opposed to the essential? Unless it is more<br>than 9/10 of all effort, shrinking all the accidental activities to zero<br>time will not give an order of magnitude improvement.

An exception

That meant that when, in a specific context many, many years later, I<br>experienced another profound change in productivity for a lot of software I<br>write, I was so surprised that I almost didn’t notice. When I eventually did,<br>and tried to explain to other people the difference, they also seemed baffled.<br>The context? Multi-threaded programming in Rust. That experience is what<br>informs my opinion on the best course for programming languages in the future,<br>so I need to convince you that there is something deep in the way that<br>Rust makes multi-threaded programming much easier.

Let me start with a concrete example. I wrote the software that builds the<br>website you’re currently reading as normal single-threaded code. Because<br>I’m lazy – and my website isn’t that big – every time I run it, the<br>entire...