In the first chapter of Girard's Proofs and Types (1989) one finds the following remarks:
Theoretical Computing is not yet a science. Many basic concepts have not been clarified, and current work in the area obeys a kind of “wedding cake” paradigm: for instance language design is reminiscent of Ptolomeic astronomy — forever in need of further corrections. There are, however, some limited topics such as complexity theory and denotational semantics which are relatively free from this criticism.
Leaving aside the question whether these comments were correct in their day, is Girard's assesment of the theory of computation valid today?
I am aware that this is quite a broad question with no definite answers. However, as his remarks seem to be rather controversial, I was hoping to get some knowledgable perspectives on his claims from someone who has an overview of the current state of affairs – which I certainly don't have.