To add to other user's comments, linear types are useful for reasoning exactly about (some) imperative constructs, which is really, really hard to do with stand

To add to other user's comments, linear types are useful for reasoning exactly about (some) imperative constructs, which is really, really hard to do with standard type systems. That's why reliably guaranteeing e.g. why it's still difficult to ensure safe and timely disposal of database connections in Haskell (maybe not now) or Scala, despite their powerful type systems. There's many other such modal type systems/logics used for other special purposes like temporal logic.