3. Rust's Top-Level Logic and Design

Rust’s top-level design doesn’t come from industry patches (like Java adding GC to address C++ pointer issues); it comes from type theory and mathematical logic.

To really understand Rust’s “way,” you need to see it through Curry–Howard correspondence: programs are proofs, types are propositions.

Here is the core chain of Rust’s top-level design:

---

First layer: Worldview — Affine type system

Affine type systems are an extension of linear type systems, mainly used in type theory in computer science to precisely control how often program resources (memory, file handles, network connections) are used.

Java/JS/C assume a world of sharing: once data is created, many pointers can point to it at once. Rust’s top-level logic is built on a variant of linear logic, namely affine types.

• Traditional (Java/JS): Data is “information.” Information can be copied. I tell you a secret; we both know it.
• Rust: Data is “physical resource.” If you have a gold bar and give it to me, you no longer have it. You can’t duplicate it (except at the cost of Clone).

Top-level conclusion: Rust doesn’t treat memory as “just memory”; it abstracts it as ownership.

• Corollary 1: Every value must have exactly one owner in the logic.
• Corollary 2: An assignment (let a = b) is no longer “copy value” but “transfer ownership” (move semantics).
• Theoretical basis: This corresponds to the assumption in linear logic that a resource can be consumed only once. That eliminates “double free” and “dangling pointer” at the root: after a resource is transferred, the original owner no longer has it, and the compiler forbids the original owner from using it again.

Second layer: Concurrency — Aliasing XOR Mutability

In computer science, most state-management disasters come from combining:

1. Aliasing: Multiple places accessing the same data.
2. Mutability: The data can be modified.

Java/JS: Allow aliasing and mutability. To avoid chaos we add runtime locks (synchronized) or a single-threaded event loop. Haskell (pure): Allow aliasing but forbid mutability (immutable). Rust: To get high performance (no GC), memory safety, and lock-free concurrency, we must break this combination at compile time.

• Rule: &mut T (mutable reference) is exclusive. &T (shared reference) is read-only.
• Implication: When there is one writer, there must be no other readers; when there are readers, there must be no writer.
• Result: Rust pushes “read-write lock” logic into the type system. Code that compiles is a mathematical guarantee that “at no time will there be a data race.”

Third layer: Compiler as theorem prover

In Java, the compiler is a translator (code → bytecode). In Rust, the compiler is a theorem prover.

When you write a line of Rust, you’re building a mathematical proof.

• Function signature is the proposition.
• Function body is the proof.

Example: Lifetimes You might find lifetime annotations 'a annoying. At the design level they’re solving inequalities. (Lifetimes are explained in detail later.)

• fn strict<'a>(x: &'a str) -> &'a str
• The compiler builds constraints: lifetime(x) >= lifetime(return value).
• If in your code x outlives the return value, those inequalities have no solution (contradiction).
• A compile error is essentially: “Your proof is inconsistent; there is a counterexample.”

That’s why Rust is hard: you’re writing business logic and at the same time submitting a “memory-safety proof” to the compiler via the type system.

Fourth layer: Trait system and isolating behavior (Traits as bounds)

(This is harder; you can reread after the later chapters.)

Java uses interface for behavior, which usually means vtables and runtime cost. Rust uses a Trait system similar to Haskell type classes, implemented at the systems level.

A Trait is a set of methods a type can implement; it’s like an “interface” in other languages—what a type can do. It’s a contract between types. Rust monomorphizes Trait code at compile time, so there’s no runtime cost.

In Rust, Send and Sync are two core marker traits for concurrency safety. They are inferred by the compiler and used at compile time to prevent data races.

Common types like i32, String, and Vec implement both Send and Sync.

Reasoning:

• Send and Sync: These are where Rust’s “higher-dimensional” design shines.
• Send: A type whose ownership can be transferred across threads.

• Sync: A type that can be shared by reference across threads (thread-safe).

• The trick: These traits are auto-derived (auto traits). The compiler recursively scans your struct’s fields:
• If all fields are Send, the struct is Send.
• If you use a non-thread-safe pointer (e.g. Rc, which doesn’t implement Send), the compiler marks the whole struct as !Send.
• Result: If you try to send a non-Send value to another thread, the compiler stops you: “The type system says this value cannot be sent across threads safely.”

use std::rc::Rc;
use std::thread;

fn main() {
    let rc_value = Rc::new(5);

    // Error: `Rc<i32>` cannot be sent between threads safely
    // Because multiple threads modifying Rc's refcount would cause a data race
    thread::spawn(move || {
        println!("{}", rc_value);
    });
}

This is very different from other languages. In Java you find out at runtime with an exception or deadlock; in Rust, concurrency safety is “derived” the moment you define the type.

Summary: The big picture above the language

1. C/C++: Libertarian. Trust the programmer; compiler just translates.
2. Java/Go: Paternalistic. Programmers make mistakes; we use GC and VM at runtime, trading performance for safety.
3. Rust: Rule of law (formal verification).

• It establishes an axiom system (ownership, borrowing, lifetimes).
• The compiler is the enforcer. It doesn’t care about your business logic; it only checks that your code obeys the axioms.
• Unsafe Rust is the only “pardon.” As in Gödel’s incompleteness, some truths can’t be proved inside the system. Rust lets you mark a region with unsafe: “I (the programmer) guarantee this; compiler, stay quiet.” This is essential for drivers and low-level hardware.

Suggestions for deeper understanding:

As an advanced programmer, don’t treat Rust only as a language; treat it as “logic puzzles under these constraints.”

• When the borrow checker complains, don’t ask “how do I work around it?” but “Where in the memory-access graph is there a cycle or conflict?”
• Read short summaries on linear type systems or look at Cyclone (a spiritual ancestor of Rust).

Rust’s beauty is that it shows: without garbage collection, strict logical reasoning and static analysis are enough to build safe and efficient systems. That’s a real theoretical breakthrough, implemented in practice.