[throwaway81523]

Linear logic is logic where any value must be used exactly once, i.e. if a=3 and you say b:=a, then b becomes 3 and a becomes undefined. The value is moved rather than copied. That is useful for describing e.g. resource management systems. If I transfer a resource to you, then you have it but I no longer do. Linear types basically means a type system that enforces linear logic.

A good practical description of linear logic (but not types) is here: https://hashingit.com/elements/research-resources/1994-03-Fo...

Yes it's about how Forth implements linear logic without realizing it ;).

[gadmm]

Baker's paper is visionary in that it announces a link between linear logic and move semantics for resources more than a decade in advance. As we know this was put into practice by C++ and Rust. Compared to linear types, it amounts to operating a change of perspective from the quantitative interpretation (is it copied? is it dropped?) to a qualitative one (how is it copied? how is it dropped?). This is very much in spirit of linear logic (though it takes a bit of work to relate these ideas to Girard's mathematics). It answers questions that linear types were never able to, such as how to mix linearity and control. I take this paper as an example that there is more to linear logic than linear types!