In the Agent Era, Why Is Rust the Go-To for AI Programming?

AI large models are reshaping programming, and many developers are starting to worry: is my skill set still valuable? Does programming language design still matter? An article shared by a Bilibili creator—"What Agents Mean for Rust, or Vice Versa" by Nick Matzakis (a core member of the Rust team)—addresses exactly these existential concerns. The author starts from his fifth-grade experience programming on a 5MHz x86 processor, pointing out that the essence of programming has not changed for years—until the emergence of AI agents brought a genuine upheaval—both exciting, and frightening and disorienting.

In the Agent Era, Why Rust Is Favored

Rust's popularity data is convincing in itself: Rust ranks second among the fastest-growing languages, with TypeScript's year-over-year growth reaching 1200%; even more striking, the amount of Rust code Meta engineers wrote this year is twice the total of the past nine years combined. David Turner emphasizes that part of the reason is that agents make it easy to try things out, and another part is that Rust is known for high performance—if choosing any language is about equally difficult, why not choose the one that executes faster?

The author believes there is a third layer of reason: Rust happens to be extremely well suited to agentic coding. He proposes three pillars of an efficient software factory—design, construction, and optimization. Rust has a natural advantage in optimization: it delivers excellent performance by default while retaining many tunable levers, such as precise control over whether data is allocated on the stack or the heap, where pointer indirection occurs, forcing a specific memory layout for structs, and even embedding inline assembly. Performance tuning used to carry an air of mystery, but today agents make this process much easier—engineers working on ultra-high-performance cryptographic algorithms say they are shifting from hand-tuning assembly to having agents do the same work; when building network services, combined with profiling tools like Dial, agents can effectively identify async performance pitfalls such as long polling and blocking.

Reliability Always Reigns: The Type System Is the Agent's Guardrail

Performance attracts people to Rust; reliability keeps them there. OpenAI's Greg Brockman once said that Rust basically guarantees correctness when it compiles, making it an ideal language for building agents. The author agrees with this judgment: languages like Rust, OCaml, and Haskell have a feeling of "if it compiles, it runs," and agents benefit from this as well.

Testing alone is far from enough—tests can prove the existence of defects but cannot prove their absence. The author often encounters situations where the first few tests look perfect and then the next test goes completely off the rails; on deeper investigation, it turns out the agent completely misunderstood the logic he was trying to express. This is precisely the real advantage of a type system: it provides guardrails that keep the agent on the right track. In Rust, guardrails are not limited to technical checks like whether field names are correct; they extend to higher-level guarantees such as "never manually close a socket."

But type systems also have inherent limitations: they can only guarantee that you have not made a mistake, not that you have done the right thing. To go further, you need proof systems. The Rust ecosystem already has a number of interesting proof tools that can prove code will not panic, and can add assertions to verify that code actually computes the expected results.

The type system is a set of rules in a programming language that classifies and constrains values, expressions, and variables according to program structure and usage. Its core role is to detect and prevent illegal operations at compile time rather than at runtime. From simple type systems that only distinguish integers from floating-point numbers, to the strong type systems with parametric polymorphism, algebraic data types, and ownership/borrow checking used in Haskell, OCaml, and Rust, the constraints grow stronger at each level. The type checker traverses the entire program before the code actually executes, constructs type inference, and verifies that every operation satisfies the established rules. Therefore, any program that compiles has, within the scope of what has been proven, ruled out an entire class of errors—for example, adding a string as if it were a number, accessing freed memory, or violating an interface contract. This is the technical source of the intuition that "if it compiles, it runs": a type system is essentially an automated, low-cost, lightweight proof that moves many defects that would otherwise surface only at runtime forward to the writing stage. And it is precisely this certainty that makes it a natural guardrail for constraining AI agent behavior.

Formal Proof: Making Unsafe Code No Longer Nerve-Wracking

Deploying formal proofs not only ensures correctness but also improves development efficiency—this sounds counterintuitive, but it is true. Some cryptographic algorithms have a very clear mathematical structure, and you can basically tell the agent: implement it however you like, as long as you can prove the code still computes the correct result; these proofs can be done with theorem provers such as Lean or ARC.

A typical scenario is Unsafe code: people sometimes use it to improve performance but remain nervous when deploying it, because if something goes wrong the risk far outweighs the benefit. If formal proof tools can verify that Unsafe code is actually safe, then all kinds of optimizations can be made without worry. So, if we have proof systems, do we still need type systems? The author's answer is absolutely yes—type systems are much simpler to use and therefore more popular; only by using type systems to eliminate all kinds of headache-inducing bugs can you focus your proof efforts on the parts that truly matter.

Formal proof is a technique that uses mathematical methods to rigorously argue that a program satisfies specific properties. Unlike the sampling-based verification of testing, it requires logical derivation of the program's behavior across all possible inputs and all possible execution paths. A common approach is to translate program semantics into logical propositions and then use theorem provers (such as Coq, Lean, or Isabelle) or tools such as dependent refinement types and SMT solvers to complete machine-checkable proofs. The Rust ecosystem already has tools such as Kani, Creusot, Prusti, and Verus, which can respectively verify that code does not panic, has no undefined behavior, satisfies function preconditions and postconditions, or computes the expected results. The cost is that writing proofs and maintaining specifications requires extra effort, and proof tools often lag in supporting language features. Therefore, formal proof in practice is usually used only for modules with extremely high correctness requirements, such as cryptography, operating system kernels, and safety-critical systems, as a second line of defense beyond the type system rather than a replacement for it.

The unsafe keyword in Rust does not disable the borrow checker or the type checker; instead, it unlocks five operations that the compiler cannot automatically verify: dereferencing raw pointers, calling unsafe functions, accessing or modifying mutable static variables, implementing unsafe traits, and accessing union fields. These operations require explicit annotation because the compiler cannot prove they are safe; the responsibility for correctness is transferred to the programmer, who must personally ensure that Rust's aliasing and memory safety rules are satisfied. If violated, the program may produce undefined behavior, the consequence of which is that the compiler is authorized to perform arbitrary optimizations, manifesting as hard-to-reproduce crashes, data corruption, or even security vulnerabilities. Typical uses of Unsafe code include implementing low-level data structures, FFI boundaries for interacting with C, and performance-sensitive cryptographic primitives. The industry usually controls risk by encapsulating unsafe code within small, reviewed safe API boundaries, which is exactly why the article emphasizes that libraries have a responsibility to protect users from undefined behavior.

The North Star Goal: No More Unsafe Code

The author proposes a North Star goal for Rust: no more Unsafe code. He does not mean never using the unsafe keyword, but rather having the ability to prove that all Unsafe code written is correct and will not cause undefined behavior. Simply knowing clearly which code needs review is itself a huge step forward; libraries have a responsibility to protect users from undefined behavior through safe API boundaries. Given the ability of AI agents to find vulnerabilities, if we want to curb the endless stream of vulnerabilities, we must raise our own technical level.

Design remains an open question. The current mainstream approach is Markdown-based development practice—writing documentation and expecting the agent to pay attention. The author is not sure how much Rust can contribute in these areas, but believes some steps can be taken: providing a way to separate interfaces from implementations so interfaces can be reviewed independently, or more clearly viewing the changes an agent has made to an interface, or providing better review tools. He also believes there is room for a language specifically for design—a tool that lets you rapidly iterate on high-level designs and invariants with an agent without diving into code details.

Design Language: The Most Critical Breakthrough

The author recommends MacBlock's article "What's Easy Now, What's Hard Now," which points out that the more clearly a task's success criteria can be defined, the easier the task is to complete. Tasks traditionally considered difficult will soon be automated, and tasks once seen as simple may become more valuable. From the perspective of programming languages, the most critical breakthrough will come from design languages—tools that capture architecture and intended behavior at a very high level, with the goal of letting humans intuitively specify designs and automatically translate them into effective verification mechanisms, such as type checking, linting, or theorem proving; then agents are responsible for translating the design into code written in traditional languages (such as Rust), with humans only needing to review occasionally.

This does not mean traditional programming language design is no longer fascinating, but the trade-offs in design are very different from before. Rust's mission remains clear: low-level enough to write kernels, high-level enough to build applications. Evolution around agents means a certain degree of noise can be tolerated—for example, explicit calls to clone or share must not be too numerous, because we still want the normal path of the code to be clear. Combined with profiling tools, you get an efficient feedback loop that makes code run faster.

The relationship among proof systems, theorem provers, and type systems can be understood as a continuum of strength and cost. Type systems are the most automated and lowest-cost kind of proof: developers only write code, and the compiler performs the checking automatically. Theorem provers require specifications and proof scripts to be written manually or semi-automatically; they have the greatest expressive power but also the highest barrier, making them suitable for verifying subtle algorithms or concurrency protocols. In between are dependent types, refinement types, and design by contract, which allow finer-grained properties to be embedded in types or annotations and verified automatically or semi-automatically by solvers. These three do not replace one another: type systems are responsible for cheaply and broadly ruling out common errors, proof systems are responsible for providing rigorous guarantees for a few critical modules, and the artifacts of proofs can themselves be used by agents as constraints to generate and modify code. Only by understanding this layering can one understand why the author insists that even with proof systems, type systems are still absolutely necessary.

One-line Summary

Rust has become the ideal language for the agent era thanks to performance, reliability, and type guardrails, and design languages will be the key breakthrough.

Paragraph Summary

The article centers on Nick Matzakis's "What Agents Mean for Rust, or Vice Versa," discussing the impact of AI agents on programming and programming language design. Rust ranks second among the fastest-growing languages, and the amount of Rust code Meta engineers wrote this year is twice the total of the past nine years combined; its high-performance defaults and tunable levers happen to complement agents' performance optimization capabilities. The author emphasizes that reliability is what keeps developers: languages like Rust, OCaml, and Haskell have the property that if it compiles, it is basically correct, and the type system provides guardrails for agents but cannot prove the program does the right thing. Therefore formal proof is needed as a supplement, especially in Unsafe code scenarios where it can eliminate deployment concerns. The author proposes a North Star goal—the ability to prove the correctness of all Unsafe code—and believes the most critical breakthrough will come from design languages: humans intuitively specify high-level designs, and agents translate them into code in traditional languages.