I can only speak as a user of linear types, not as a type theorist. They are extremely useful in practice. In ATS they enable not just tracking memory but any form of resource that needs to be cleaned up. If you fail to do so you get a compile time error.<p>This removes much of the burden of wondering if you got the resource management right. Especially when maintaining existing applications. If you refactor things the compiler tells you when you got it wrong.<p>There is overhead since you are managing resource manually - both syntax-wise and mental though.<p>For concurrency they enable &#x27;solving&#x27; shared state by making it difficult to share state. You really have to pass ownership of the resource to the other thread so it can no longer be accessed anywhere else.