"The attractiveness of logic programming, when it was first launched, was that it had a ready-made declarative reading, which was expected to make a big differe

"The attractiveness of logic programming, when it was first launched, was that it had a ready-made declarative reading, which was expected to make a big difference for programming. Unfortunately, Prolog also had a bad procedural reading that people struggled with. So, in practice, Prolog programmers spent almost all of their effort on the procedural meaning, and the declarative meaning went out of the window. In the end, Prolog was a good dream, but a bad reality. Coming to classical logic per se, I believe it is ill-fit for describing computer programs or "processes" as you call them. First of all, classical logic doesn't have any well- developed notion of time or dynamics, and it has a nasty existential quantifier which assumes that all things exist once and for all. In computer systems, new things come into being all the time, well beyond the time of the original development or deployment. We know how to write computer programs that deal with that. Classical logic doesn't. (LEJ Brouwer made this criticism a long time ago in the context of mathematics. There it might have been just a philosophical problem. But in Computer Science, it is a practical problem.) I believe logicians of philosophical inclination are prone to be enamored with what they have and lose sight of what they don't have. For a good part of two millennia, they kept debating Aristotilean syllogisms, without realizing that classical logic was yet to be discovered. Finally, it was left to the mathematicians to formulate classical logic. The logicians of today are similarly enamored with classical logic without much of an understanding of what it lacks. We would be ill-advised to listen to them. Or, we would be stuck for another two millennia, God forbid. [By the way, the Wikipedia page on Classical Logic is in a pitiful state. I hope somebody will pay attention to it.] Brilliant new things are happening in Logic. - Mathematicians have formulated Toposes (a generalization of Kripke models), which give us a great new variety of models for intuitionistic logic. There are deep mathematical facts buried in them and continue to be discovered. Toposes and intuitionistic logic are appropriate for modeling computer programs, which live in a growing dynamic world rather than a static one. - Girard has formulated Linear Logic, which broadens our idea of what kind of "things" a logic can talk about. David Pym and Peter O'Hearn invented Bunched Implication Logic, extending Linear Logic with a beautiful model-theoretic basis. These logics applied to imperative programming (which go by the name of "Separation Logic") are revolutionizing the development of technology for imperative programs. It is time to leave behind the classical logic. In fact, we should have done it a long time ago." - Prof Uday Reddy on the types mailing list. http://lists.seas.upenn.edu/pipermail/types-list/2013/001684.html http://lists.seas.upenn.edu/pipermail/types-list/2013/001684...