What agents mean for Rust (and vice versa)

Argues that humans and programming-language designers remain essential even as LLM-driven agents change how code is written, and that Rust is particularly well suited to agentic development. Presents a three-pillar view of a software factory - design, construction, optimization - and shows how Rust’s “fast by default” ethos plus explicit performance knobs (allocation control, layout, boxing, inline assembly) matches agents’ strengths: agents are already effective at profiling-driven tuning, diagnosing async pitfalls, and fine-tuning hot paths. Rust’s popularity in the agent era is attributed both to performance reputation and to its fit for workflows where agents propose PRs guided by benchmarks and profilers.

Makes the case that strong static types and the borrow checker are crucial guardrails that keep agents from producing catastrophic logic errors, but that types alone aren’t enough; proof systems are needed to establish richer correctness properties. Points to existing Rust proof tools (Verus, Creusot, Aeneas, Kani) and theorem provers used in cryptography, arguing that proofs can unlock safe low-level optimizations (including verified unsafe code). Recommends doubling down on “if it compiles, it works” by expanding the properties the type system can express, improving compiler extensibility for smoother proof-tool integration, and aiming toward eliminating unsafe code through verification.