This column introduces linear logic, a resource-conscious logic introduced by Girard in 1987. Unlike classical and intuitionistic logics, linear logic distinguishes between two types of conjunction and disjunction, and introduces a modal operator to mark reusable propositions. Linear logic avoids paradoxes by treating propositions as dynamic resources rather than static facts. For example, in a vending machine scenario, linear logic correctly captures that one dollar cannot buy two packs of cigarettes. Linear logic has two types of conjunction: multiplicative (⊗) for having both A and B at the same time, and additive (&) for choosing between A and B. It also has two types of disjunction: multiplicative (⊕) for either A or B, and additive (⊕) for someone else's choice. Linear logic also includes a modal operator ! for reusable resources and ? for non-reusable ones. Linear logic has been applied to various areas of computer science, including the encoding of Petri net reachability, functional programming languages with explicit duplication, and logic programming. It has also been used in natural language processing and concurrency models. The complexity of linear logic has been studied extensively. Propositional linear logic is undecidable, while the multiplicative-additive fragment (MALL) is PSPACE-complete. The multiplicative fragment of linear logic is NP-complete. Linear logic has been shown to be a powerful tool for studying computational complexity and compiler optimization. Linear logic has a unique feature of cut-elimination and involutive negation, making it a non-classical logic with practical applications. Current research is exploring its use as a type system for studying computational complexity and compiler optimization, as well as in logic programming, natural language processing, and concurrency.This column introduces linear logic, a resource-conscious logic introduced by Girard in 1987. Unlike classical and intuitionistic logics, linear logic distinguishes between two types of conjunction and disjunction, and introduces a modal operator to mark reusable propositions. Linear logic avoids paradoxes by treating propositions as dynamic resources rather than static facts. For example, in a vending machine scenario, linear logic correctly captures that one dollar cannot buy two packs of cigarettes. Linear logic has two types of conjunction: multiplicative (⊗) for having both A and B at the same time, and additive (&) for choosing between A and B. It also has two types of disjunction: multiplicative (⊕) for either A or B, and additive (⊕) for someone else's choice. Linear logic also includes a modal operator ! for reusable resources and ? for non-reusable ones. Linear logic has been applied to various areas of computer science, including the encoding of Petri net reachability, functional programming languages with explicit duplication, and logic programming. It has also been used in natural language processing and concurrency models. The complexity of linear logic has been studied extensively. Propositional linear logic is undecidable, while the multiplicative-additive fragment (MALL) is PSPACE-complete. The multiplicative fragment of linear logic is NP-complete. Linear logic has been shown to be a powerful tool for studying computational complexity and compiler optimization. Linear logic has a unique feature of cut-elimination and involutive negation, making it a non-classical logic with practical applications. Current research is exploring its use as a type system for studying computational complexity and compiler optimization, as well as in logic programming, natural language processing, and concurrency.