Local Reasoning for Global Properties

For the past few years, I have frequently been asked a central question: Will the evolution of AI necessitate the creation of new programming languages?

Initially, my response was "probably not." This seemed logical because AI has demonstrated an impressive ability to generate code across virtually any existing syntax. However, as the technology has matured and its limitations have surfaced, my perspective has shifted.

The Gap: Local vs. Global Logic

My observation is that current AI is excellent at producing high-quality local snippets (such as a single function), but it falters when a global understanding of the entire system is required.

The "Defensive Check" Symptom: One clear indicator of this struggle is the AI's tendency to over-use defensive checks. While these seem safe, they create a ripple effect:

• They suggest a wider range of possible states than actually exist.
• This increases the cognitive load for human readers.
• It leads to an exponential growth in perceived complexity.

If this limitation persists, we may need to return to the drawing board of programming language design.

My Objectives for this Discussion:

• Avoid predicting specific future language features.
• Identify if a language exists where local reasoning guarantees a global property.

---

Context: The Role of Programming Languages

Having spent much of my career in the realm of PL design, I am naturally inclined to champion their importance. However, I must be honest: there is little empirical evidence that a language alone creates a profound leap in software reliability or productivity.

Consider the following observation:

This suggests that the primary driver of success is not the tool, but empathy—the ability to understand exactly what the user needs and implement it reliably.

"Most of the big past gains in software productivity have come from removing artificial barriers that have made the accidental tasks inordinately hard, such as severe hardware constraints, awkward programming languages, lack of machine time." — Fred Brooks (The No Silver Bullet Argument)

The Productivity Equation

When I transitioned from Assembly to languages like C or Python, my productivity skyrocketed. Assembly forced me to obsess over low-level minutiae, causing me to lose sight of the high-level architecture.

However, I realized that such a leap is rare. If we define the total effort as $E$, and the "accidental" complexity as $A$, then: $\text{If } A < \frac{1}{10} E, \text{ then reducing } A \text{ to } 0 \text{ will not yield an order-of-magnitude gain.}$

---

The Rust Exception

Despite my skepticism about "silver bullets," I encountered a surprising shift in productivity while using Rust. To illustrate this, let's look at the architecture of my website builder.

The Evolution of the Site Builder

Initially, the software was written as a standard single-threaded application. Because the site is small, I simply rebuild everything on every run. Eventually, the pauses became too long, hindering my editing flow.

In almost any other language, moving to multi-threading is a nightmare. My history with concurrency is a trail of:

1. Hard-to-trace crashes.
2. Heisenbugs that appear weeks later.
3. General dread of "threading horrors."

The Result in Rust: The rewrite took less than 5 minutes. It worked perfectly on the first attempt, has remained stable, and—most importantly—I had absolute confidence in its correctness.

While Rust is not a flawless language, it achieves something profound: it allows the developer to reason about a small piece of code (local) and receive a guarantee about the thread-safety of the entire program (global).

Figure 1: The conceptual bridge between local constraints and global properties.