The reasoning is sort of a technical analogy. Linear Logic was discovered by an analysis of the structure of Coherent Spaces, which are a model of Intuitionisti

The reasoning is sort of a technical analogy. Linear Logic was discovered by an analysis of the structure of Coherent Spaces, which are a model of Intuitionistic logic distilled from Scott domains. Jean-Yves Girard realized that function spaces A => B can be decomposed into two finer constructions as !A -o B where `A -o B` is a space of functions whose properties resemble linear functions between vector spaces and `!A` resembles the Fock space construction on a vector space. There are two ways this resemblance manifests. First off, the basic elements of a coherent space are called cliques which are analogous to vectors in a vector space. The functions constituting the coherent space A => B preserve directed unions of cliques but the linear functions of A -o B preserve arbitrary unions of cliques which is strongly analogous to preserving arbitrary linear combinations of vectors. Second off is that you can build a symmetric monoidal category out of coherent spaces and vector spaces are the archetypal symmetric monoidal category. There are models of fragments of Linear Logic where the linear functions are literally polynomials of degree 1, but in its full generality it doesn't quite match exactly with linear algebra. Nonetheless the metaphor goes deep and you can even capture notions of differentiability in extensions to the logic. For a technical exposition you can read this paper by a guy who's applying this sort of stuff to machine learning: https://arxiv.org/abs/1407.2650 https://arxiv.org/abs/1407.2650 I apologize if this is all too obscure to justify the name. Linear Logic's applications to programming were sort of secondary to its proof theoretic novelty at its inception.