Categorical Models of Linear (and other) logics

I've read with interest the discussion of categorical models 
of linear logics.  I've wrapped my brain around the recent
results, and I've enjoyed it immensely.  I do have a question
about categorical models, however, and I think that this 
list is as good a place as any to have them answered.  
My question is this.  

* What are categorical models of logics good for?

Possible answers are as follows.

1. They help us understand our term assignment systems for 
   these logics.

2. They help us prove results about our logics, as we can 
   use category theory.

3. We can show that our favourite logic corresponds to some
   already-found structure in category theory, and hence, our
   logic gets brownie-points for being `natural.'

4. The category (or class of categories) we are interested in
   is the *intended model* for our logic.  That is, we are using
   our logic to model some phenomenon, which we have already 
   presented categorically.  As we have shown that this category
   (or class of categories) is a model of our logic, we thereby
   show that our logic models nicely the phenomenon of interest.

Are any of these answers correct?  If so, which of them?  
Or are they missing the point?  Are categorical models interesting
for some other reason?  

I'd be very interested if there are any results like those
foreshadowed in answer `4' actually appear in the literature on 
linear logic.   The most I can find is answers in the ballpark
of 1, 2 and maybe 3.  

Replies can be sent to the list, or to me.  Either is fine.

Thanks a bundle,

Greg Restall

Redemption rips through the surface | gar@arp.anu.edu.au  Automated Reasoning
of time in the cry of a tiny babe.  | Project, Australian National University
                 - Bruce Cockburn.  | Canberra, ACT 0200, Australia.