Substructural Logics

Rust guarantees memory safety without a garbage collector, through linear types baked directly into the type system. This is not just a practical trick: it is Girard's 1987 theorem, instantiated in a production language.

• **Rust ownership:** the ownership system = affine types; the borrow checker = proof checker in separation logic
• **Facebook Infer:** a static analyzer based on separation logic, finding null dereferences and memory leaks in production code at Meta/Amazon
• **Quantum computing:** linear logic models quantum circuits (quantum states cannot be cloned, the no-cloning theorem)

Предварительные знания

• Natural Deduction
• Intuitionistic logic

Structural Rules and Their Absence

Rust's borrow checker enforces linear logic: each value is consumed exactly once (no weakening, no contraction) , 250,000 lines of implementation. Classical and intuitionistic logic silently use three **structural rules** of the sequent calculus: weakening, contraction, and exchange. Substructural logics drop some of these, producing logics with fundamentally different properties.

Without weakening: hypotheses cannot be 'ignored', each must be used. Without contraction: hypotheses cannot be 'copied', each is used exactly once. This models resources: money, time, physical objects.

Girard's Linear Logic

Linear logic (Girard, 1987) is the logic of **resources**: each formula is a resource that is consumed upon use. '$1 → cookie' can be used only once. Girard also showed that classical logic embeds into linear logic via modalities!