Logic texts for computer scientists

A student in my graduate Type Systems course was asking about sources
for background reading in relevant areas of logic.

There is, of course, the old standby -- Girard, LaFont, and Taylor's
Proofs and Types.  Hindley's new book (Basic Simple Type Theory) has a
careful explanation of the Curry-Howard isomorphism.  And I'm told
that Taylor's brand-new book, while rather technical, has some good
material.  But I'm still wondering whether the ideal book or survey
article is out there -- a broad introduction to logic "from a
computational perspective" and aimed at nonspecialists.

Does anyone have any good tips?  Please reply directly to me; I'll
summarize for the Types list.