The difference between the two is that in the "bunched" style, hypotheses in the context are decorated with resource expressions, and in the "linear" style, they are decorated with merely resource variables, sort of a special case of the former. However, if the whole system is in this special case, the cut principle is different, and the left/elimination rules for additive conjunction are different. So lately I've been focussing on the meaning of additive conjunction in the two systems.
The idea I had last night was that linear &, with respect to bunched ^, has a property that is kind of like intuitionistic logic with respect to classical logic on the conclusion side of the turnstile. The commitment to one choice or the other is like the commitment to one intuitionistic disjunct or the other. Bunched logic lets you keep both conjuncts around, and classical logic both disjuncts. This bolstered my feeling that linear & ought to be something kind of like @A ^ @B for some possibilityish modality @, by analogy with the modal translation of intuitionistic into classical logic, or else maybe ^ is representable as #(A & B) for some operation # that throws away information kind of like double-negation does.
These are really just hazy intuitions, though; setting up a system that actually satisfies cut elimination is being really hard. There's so many places, in the usual game of pushing around the bubble-in-the-wallpaper of proof obligation, for the bubble to hide.
Better stop before I reach Girard-like levels of crazy metaphors...
