docs: add insights on Rust ownership, borrowing, traits, and lifetimes to AGENTS.md

Author: kosiew

AGENTS.md

@@ -28,6 +28,58 @@ This repository contains Python bindings for Rust's DataFusion.
 - The repository mixes Python and Rust; ensure changes build for both languages.
 - If adding new dependencies, update `pyproject.toml` and run `uv sync --dev --no-install-package datafusion`.
 
+## Rust insights
+
+Below are a set of concise mental-model shifts and expert insights about Rust that are helpful when developing and reviewing the Rust parts of this repository. They emphasize how to think in terms of compile-time guarantees, capabilities, and algebraic composition rather than just language ergonomics.
+
+1. Ownership → Compile-Time Resource Graph
+
+> Stop seeing ownership as “who frees memory.”
+> See it as a **compile-time dataflow graph of resource control**.
+
+Every `let`, `move`, or `borrow` defines an edge in a graph the compiler statically verifies — ensuring linear usage of scarce resources (files, sockets, locks) **without a runtime GC**. Once you see lifetimes as edges, not annotations, you’re designing **proofs of safety**, not code that merely compiles.
+
+2. Borrowing → Capability Leasing
+
+> Stop thinking of borrowing as “taking a reference.”
+> It’s **temporary permission to mutate or observe**, granted by the compiler’s capability system.
+
+`&mut` isn’t a pointer — it’s a **lease with exclusive rights**, enforced at compile time. Expert code treats borrows as contracts:
+
+* If you can shorten them, you increase parallelism.
+* If you lengthen them, you increase safety scope.
+
+3. Traits → Behavioral Algebra
+
+> Stop viewing traits as “interfaces.”
+> They’re **algebraic building blocks** that define composable laws of behavior.
+
+A `Trait` isn't just a promise of methods; it’s a **contract that can be combined, derived, or blanket-implemented**. Once you realize traits form a behavioral lattice, you stop subclassing and start composing — expressing polymorphism as **capabilities, not hierarchies**.
+
+4. `Result` → Explicit Control Flow as Data
+
+> Stop using `Result` as an error type.
+> It’s **control flow reified as data**.
+
+The `?` operator turns sequential logic into a **monadic pipeline** — your `Result` chain isn’t linear code; it’s a dependency graph of partial successes. Experts design their APIs so every recoverable branch is an **encoded decision**, not a runtime exception.
+
+5. Lifetimes → Static Borrow Slices
+
+> Stop fearing lifetimes as compiler noise.
+> They’re **proofs of local consistency** — mini type-level theorems.
+
+Each `'a` parameter expresses that two pieces of data **coexist safely** within a bounded region of time. Experts deliberately model relationships through lifetime parameters to **eliminate entire classes of runtime checks**.
+
+6. Pattern Matching → Declarative Exhaustiveness
+
+> Stop thinking of `match` as a fancy switch.
+> It’s a **total function over variants**, verified at compile time.
+
+Once you realize `match` isn’t branching but **structural enumeration**, you start writing exhaustive domain models where every possible state is named, and every transition is **type-checked**.
+
+Stop seeing `Option` as “value or no value.” Instead, see it as a lazy computation pipeline that only executes when meaningful. These combinators turn error-handling into data flow: once you think of absence as a first-class transformation, you can write algorithms that never mention control flow explicitly—and yet, they’re 100% safe and analyzable by the compiler.
+
+
 ## Refactoring opportunities
   - Avoid using private or low-level APIs when a stable, public helper exists. For example,
     automated refactors should spot and replace uses: