"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."
Fwiw, answer-set programming is a logic-programming language with a Prolog-derived syntax that has only a declarative reading, and no procedural reading.
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...