Another issue that I want to stress is the distinction between universal and special purpose formal systems. So as we have said there is a plethora of formal systems in computer science.
Many of these claim to be universal models, or Turing complete, in the sense that they can model any other formal system, actually they can model any system.
But experience in Formal methods has indicated that there is no chance to come up with the ultimate unique logical system. On the other hand, we really have to give up any hope of getting back to some kind of Reductionist Paradise, some kind of universal formal system, really in the tradition of Leibniz, a unique system that is capable of handling all different situations.
We have, on the other hand, to learn to live with the multitude of different systems and special purpose formalisms.
And we have to be ready to conceive mutually irreducible different frameworks. And this is particularly so in the crucial area of concurrency, security and mobility, especially in the area so called "global computing".