A couple of years ago, I was thinking how fabulous it would be if JeanYvesGirard wrote a book that would explain logic from ground zero all the way up to proof theory, types, linear logic and so on, so forth. I was hoping that the extraordinary erudition and amazing writing talent exposed by the author in fragmentary but absolutely briliant articles, would make it to the many readers who would want to learn from the great mathematician. In contrast, a lots of software engineers have been influenced by either dry and technical course books, or muddled pseudo-science like GoedelEscherBach.

Now this wish has almost come true in the form of Lecture Notes for a course in ProofTheory that Girard just published on the web, both in French (the original)
 http://iml.univ-mrs.fr/~girard/cours/cours.html 
and English 
 http://iml.univ-mrs.fr/~girard/coursang/coursang.html. 
Although it's not a formally published book, and especially the English translation could use some minor editing, it's probably the next best thing, and much better than books on the same subject from other authors. The notes are a little bit demanding on the reader -- you have to be familiar with mathematical logic 101 to know where he's driving at, and a solid general culture is also helpful to get the many parallels that the author uses to convey important intuitions. But the reward is plentiful.

Reading these one can discover a fabulous spirit: his technical mastery of the material, which is presented in the most economical and elegant way, is enhanced by a wealth of unexpected connections and cultural references to the point where there's doubt if you read lecture notes or a novel by Umberto Eco. Girard's cultural horizon spans the history of antiquity, philosophy from the classics to the moderns, the theological controversies of the Christian Church, all the way to Stanley Kubrick and Arthur Clarke. More importantly, unlike any other books that I've read (must be 5 or 6) Girard, gives you a sense of direction, you get a very solid intuition behind the many technicalities, a hystorical retrospective on the evolution of logic as well, and with Girard's lecture notes you can pretty much be sure you are not sent on the wrong tracks. 

For me, reading Girard on logic, is the same kind of enlightening experience as reading Dijkstra's EWD manuscripts. Girard also resembles Dijkstra in the rather blunt style with which he chastises and ridicules a lot of false starts and misleading directions in the field of logic. In particular some areas of ArtificialIntelligence and all kinds of "logics" that tried to circumvent Goedel's theorem. --CostinCozianu