The Coq mailing list

["Robert L. Constable" <rc AT CS.Cornell.EDU>]

All,

With respect to why constructive logics are interesting in computer
science, I would surely mention that the rules about programming
language data types are well expressed in constructive logics because
the semantics of these logics is computational.  For example, in
programming languages, we take the function type A -> B to be computable
functions (for partial functions we use in Nuprl the A -> barB type);
this is the meaning given to the type in constructive type theory.  The
same can be said about recursive types, intersection types, and records
--- the programmer's understanding is computational and accords well
with that given by constructive logic.

Logicians often use the term "Intuitionistic logics" only to refer to
those which include concepts that cannot be interpreted in classical
logics, such as free choice sequences.  Intuitionists also use stronger
principles to reason about funtions over the computable real numbers,
for example asserting that they are all continuous.  In contrast,
constructive logics can be completely compatible with classical logics
and can be read in a way that keeps track of computational meaning.

Generally I would say that constructive logics allow people to
conveniently express distinctions and concepts that arise naturally in
computer science, such as computability, decidability, reducibility,
data type, etc.  Classical concepts can be conveniently added to
constructive logics, and there might be an argument that the converse
direction is harder in some sense; a constructivist would argue that
they cannot be added faithfully.

Of course, one of the strongest reasons for formalizing and implementing
constructive logics such as Alf, Coq, Lego, MetaPRL, Nuprl, etc. is that
in those systems we can write programs by extraction from proofs.  This
is an elegant way to provide a correct-by-construction programming
methodology.  The Coq community has demonstrated just how powerful this
methodology can be.  A similar methodology for orrect-by-construction
programming has become a goal for researchers in concurrent and
distributed systems and for real-time programming.

The research agenda that explores the role of constructive logics in
computer science is even more rich now than when it emerged in the 70's.
We are able to provide extremely rich programming environments (I
sometimes call these Logical Programming Environments); we can express
computational complexity notions in the logics, and those allow us to
reason about resource use.  Thus these logics can help us organize our
knowledge about algorithms as well as data types.  We can study partial
functions and partial objects.  We can provide a plausible semantics for
classes and objects.

The work of Ranta on natural language semantics shows that the role of
these logics in computer science is broader than programming language
semantics and methodology.  The philosophical value of constructive
logics suggests that they play a role in understanding the foundations
of computing and information science as well as the foundations of
mathematics.  There are even people who believe that constructive logics
will also play a key role in the formulation of physics in terms of
information and computation (in the sense of Wheeler).

The question driving this discussion is one that continues to fascinate
people for many reasons.  Perhaps we'll learn of more reasons in this
forum.

Bob Constable