Much like all dynamically typed languages are poor statically typed languages, typed functional programming languages (corresponding to intuitionistic logic) are subsumed by linear logic. Girard articulates this unity in the logical context. Let us gloss the functional programming side of things.

Linear logic allows us to recover intuitionistic fragment via the exponential modality \( ! \). \( !A \) is the perennialization of \( A \); one translates intuitionistic formulas as

\( A \rightarrow B := !A \multimap B \\ A \vee B := !A \oplus !B \\ A \wedge B := A \& B \)

Programming languages such as ATS and Rust do things differently, associating linearity/perenniality with a named type; a value of type ptr (say) is perennial and can be duplicated and discarded as in C, while a value of type list is linear and must be used exactly once. Values which are stack-allocated or stored in registers are perennial while heap-allocated values are linear.

Though Rust focuses on manual memory management, values backed by a garbage collector fit into this scheme: functional languages correspond to intuitionistic logic, and their values are perennial and should be typed like i64 in Rust.

Conversely, functional languages could add linear types in this way, distinguishing mutable arrays or pointers as linear.

Conclusion

Any new general-purpose language without linear types is already obsolete. Users should be wary of new languages that do not bother to offer linear types.