Linear logic has been announced as revolutionary for the design of programming languages for more than 30 years. However, recent works around so-called “linear types” leave many cold. Yet, linear logic has independently developed as a central theory in denotational semantics, where it illuminated e.g. aspects of continuation-passing style, evaluation order and effects at a more fundamental level, offering fruitful links to proof theory.

The point of view of this talk is that linear types and linear logic are best seen as distinct theories applied to programming languages (each with its own kinds of questions, results and validity criteria), and moreover, that there is currently a missed opportunity in examining the practical claims of linear types through the lens of linear logic.

Some well-motivated ideas withstand examination, such as kind-based linearity, or the challenge of marrying linearity and control—providing fruitful inspiration for theory in return. Other ideas do not hold up to scrutiny, relying in essential ways on idiosyncratic and poorly-motivated interpretations of linearity, such as an alleged divide between linearity and uniqueness. Lastly, linear logic also suggests new research directions for addressing standing problems and for connecting more convincingly to modern systems programming language concepts.

The goal of this talk is to promote and disseminate useful knowledge related to linear logic within the programming language research community, and to encourage a shift in the community’s expectations regarding the proof standards for certain types of claims.