Perhaps what is most striking about Girard in contrast to Nozick is how he manages to be very rigorous and artful simultaneously. Something as abstract of logic becomes a living creature when Girard talks about it. To see logic this way is to expect it to flourish in subordination to the rest of human experience, not languish in its own obscure enclave, ceaselessly chasing its own tail, reducing the alluring to the banal.
And one can be rigorous without resorting to formulae.
The short version is that back in the late 60s, Althusser suggested that fields of knowledge inherently have "a blind spot" -- his idea was that every field of knowledge has to resort to structuring/organizational principles which cannot be properly articulated within the field of knowledge itself. Jacques-Alain Miller applied this idea to logic, arguing that the Fregean definition of equality (and hence number) exhibits precisely this kind of problem. Namely, Frege defined zero as the extension of the predicate "not equal to itself", and so Frege implicitly excludes the subject from logic, as Lacan had defined "subject" as the non-self-identical.
However, Alain Badiou objected very strongly against the extension of Althusser's ideas to logic. He thinks that science and mathematics can generate definitively true, objective, non-political knowledge, and so while blind spots can occur in daily ("ideological") life, they cannot occur in science.
Girard is essentially making an argument against Badiou and in favor of Miller. Because Girard is Girard, he never explicitly mentions any of these people in his lectures. This way, he can laugh at those of us who were too ill-informed to catch the fact that the TITLE of his lectures is a direct reference to Althusser.
Anyway, Girard begins with Lorenzen's idea that a proof can be understood as a dialogue between a proponent and a refuter, and the observation that the continuation-passing-style translation embedding classical logic into intuitionistic logic doesn't require that the answer type of the continuation be the empty type. He observes that these two ideas fit together in Krivine-style realizability models of classical logic: every formula can be interpreted as a set of proofs and refutations, and the interaction of a proof with a refutation yields a behaviour in the answer type. As a programmer, I think of the answer type as the runtime system of a programming language. The Krivine construction ensures that every proof -- every program -- both respects the invariants of the answer type/runtime system, and can never observe them.
So the runtime system of a programming language exhibits the essential structure of an Althusserian blind spot, and so via Curry-Howard so must logic.
I don't claim to understand the implications of all this, but I find the idea of bringing continental philosophy into the foundations of logic in a really serious, technically profitable way to be very exciting.
I've wanted to see this paradigm implemented in the Isbell envelope of a category, whose objects are pairs of a presheaf and copresheaf T, E and a natural transformation from T(-) x E(--) ~> Hom(-,--) . I think it would be really striking if the answer type could be Hom itself, which I like to think of as a formalisation of the turnstile |- by itself.
For example, through linear logic, one can find new justifications for logical constructions internally in contrast to justifications externally through model theory. This is clearly a philosophical program within logic. I believe it has philosophical implications outside of logic.
I think this is a serviceable explication of Girard's program as a philosophical program: http://s3.amazonaws.com/academia.edu.documents/36506773/SinT...