Skip to content

Software Quality

Linear types

Linear and substructural type systems constrain not what a value is but how it is used: how many times, and in what order. A linear type must be used exactly once; an affine type at most once. From that single rule the compiler proves, at compile time, that a resource is released exactly once, that a value is never used after it is consumed, and that no two live paths mutate the same data at once.

Rust's borrow checker is the flagship. Its affine ownership (each value has one owner, moved rather than copied) eliminates use-after-free, double-free, iterator invalidation, and data races in the safe subset of the language. Memory safety is the sharpest application of the discipline, not its whole extent.

The family is defined by which of ordinary logic's structural rules it drops: weakening (discard an unused value), contraction (duplicate a value), and exchange (reorder).

Ordinary logic keeps all three; each discipline removes some, and the remaining freedom is the usage rule:

Discipline Forbids (rule removed) Usage Where
Linear discarding and duplicating (weakening, contraction) exactly once Girard's linear logic; Linear Haskell (%1 ->); Clean; ATS; Austral; Move / Cadence resources
Affine duplicating (contraction) at most once Rust ownership + lifetimes; Swift ~Copyable; C++ move-only (unique_ptr, unenforced)
Relevant discarding (weakening) at least once rarer; "must-use" disciplines (#[must_use]-style)
Ordered discarding, duplicating, reordering (all three) exactly once, in sequence ordered logic; session-typed channels; stack and region layout

A second style, reference capabilities (Pony), types each reference by the aliasing, mutation, and sharing it permits rather than by counting uses.

The same machine-checked usage discipline pays back as maintainability: a refactor that breaks an ownership or lifetime assumption fails to compile instead of surfacing at runtime.

What it catches

  • Resource-lifecycle bugs. A file, socket, lock, connection, or transaction typed linearly must be released exactly once; the compiler catches the missing close and the double close.
  • Use-after-consume. Using a value after it has been moved, freed, or handed off fails to type-check. In Rust this is use-after-free; in general it is use-after-consume.
  • Double-free and double-release. Consuming a value twice is a type error (an owner moved out of scope twice, a lock released twice).
  • Data races. Concurrent access to mutable state without synchronization is rejected. Rust's Send / Sync bounds and Pony's reference capabilities make sharing a type-level question.
  • Aliasing and iterator invalidation. Two live paths to the same mutable data are forbidden by construction (Rust) or controlled by capabilities (Pony); mutating a container while iterating it is rejected at compile time.
  • Protocol violations. A session-typed channel enforces that a protocol's steps run once, in order; an out-of-order or skipped step is a type error.
  • Asset non-conservation. A linear resource type cannot be copied or silently dropped, so a modeled coin cannot be duplicated (counterfeited) or lost (burned by accident).

What linear types do not catch: bugs that respect the usage rules but are still logically wrong (integer overflow, business-logic errors), bugs inside unsafe blocks (Rust) or explicit allocator misuse (Zig), and panics. The proven bug class is named and scoped; what falls outside it is what tests and other methods are for. Affine typing is one attack on memory errors among several: verifying memory safety classifies the error space and maps each class to the methods and tools that close it.

Categories of substructural type system

  • Ownership and borrowing (Rust). References are tracked with lifetimes, and a mutable reference excludes shared references at the same scope.
  • Reference capabilities (Pony). Six capabilities on every reference (iso, trn, ref, val, box, tag) describe the aliasing, mutation, and sharing the holder is permitted (Clebsch et al. 2015)1. iso (isolated, unique) is the linear corner; val (immutable, shareable) and tag (opaque identity) express sharing that a pure use-count cannot. Designed for actor concurrency: safe data sharing without locks.
  • Region-based memory management (Cyclone, historical; a research influence on Rust). Allocate into a region, freed as a unit; the type system tracks region lifetimes.

Tools

Ownership and affine (systems)

  • Rust: the most widely deployed production example. Adoption in Android, the Linux kernel (drivers and core paths), Windows kernel components, Firefox, Cloudflare, and AWS Firecracker.
  • Swift: noncopyable types (~Copyable) add affine ownership with explicit consuming and borrowing; automatic reference counting (ARC) handles the rest at runtime, outside weak/unowned-reference cycles.

Linear and uniqueness (functional)

  • Linear Haskell: a linear arrow (a %1 -> b) layered on GHC; used for safe mutable arrays (mutate a unique array in place, then freeze it) and safe resource APIs.
  • Clean: uniqueness types; the design ancestor of ATS-style linearity.
  • ATS, Austral: linear types for low-level and systems code.
  • Idris 2: multiplicity quantifiers (0 / 1 / unrestricted), linear and dependent at once.
  • Mercury: unique di / uo modes thread the I/O world state linearly, giving a pure logic language deterministic I/O.

Reference capabilities

  • Pony: actor language; six reference capabilities. Niche but the cleanest production example of capability-based aliasing control, and garbage-collected, so the capabilities buy data-race freedom rather than memory reclamation.

Linear resources and digital assets

  • Move (Aptos, Sui) and Cadence (Flow) make a resource linear: it cannot be copied or dropped, only moved, so an on-chain asset is conserved by construction. The largest public deployment of true linearity.

Adjacent

  • Granule, Alms: research languages with graded / quantitative resource types (the semiring generalization of "how many times").

When to use, when not

Use:

  • For resource-lifecycle-heavy code. Files, sockets, locks, connections, and transactions typed linearly turn "released exactly once" into a compile-time guarantee.
  • For systems and security code where memory bugs are the risk profile. Rust's affine ownership eliminates the category; the Microsoft Security Response Center and Linux/Android maintainers both cite memory bugs as 70%+ of CVE-class issues.
  • For concurrent code where data races are a real risk. Rust's Send / Sync and Pony's capabilities make sharing safe by construction.
  • For protocol conformance (session types) and conserved resources or digital assets (linear resource types, Move and Cadence).

Don't:

  • For business-logic-heavy code where usage and memory bugs are not the risk profile. The fight-the-compiler cost may exceed the benefit; consider a garbage-collected language with strong types (type systems).
  • As a substitute for testing the logic. Usage safety is a named bug class; logic errors are not covered.
  • For throwaway prototypes. The cost-to-iteration tax shows up most at the exploratory phase.

Evidence

  • Industrial adoption of Rust. Linux kernel (since 6.1), Windows kernel components, Firefox, Android. Per the Android team's 2022 report, memory-safety bugs in new C/C++ code accounted for the majority of high-severity Android CVEs, and Rust adoption is part of the response.

Controlled empirical comparisons of "team writing Rust" vs "team writing C++" do not exist in the published literature. The case for linear types rests on the definitional point: a value used against its usage type cannot occur, not "has not yet been seen".

Classification

  • Quality dimensions: Functionality (resources used correctly by construction: acquired and released exactly once, never after consumption; protocols and asset conservation enforced in the type), Security (memory safety in the affine case (Rust): no use-after-free, double-free, or data race in the safe subset), Maintainability (fearless refactoring: a broken ownership or lifetime assumption is a compile error, not a runtime bug).
  • Area: Resource-lifecycle code (files, sockets, locks, connections, transactions); systems and security programming where memory bugs are the risk; concurrency; protocol conformance; conserved digital assets.
  • Guarantee: Exhaustive within the discipline: by construction, a value used against its usage type cannot occur.

Referenced by

References

  1. Clebsch, Sylvan, Sophia Drossopoulou, Sebastian Blessing, and Andy McNeil. 2015. "Deny Capabilities for Safe, Fast Actors." Proceedings of the 5th International Workshop on Programming Based on Actors, Agents, and Decentralized Control (AGERE! 2015), 1–12. https://doi.org/10.1145/2824815.2824816. ↩