[TYPES] [tag] Re: Declarative vs imperative

[Luis Caires]

On Fri, May 3, 2013 at 11:28 PM, Mark Janssen <dreamingforward at gmail.com> wrote:

> But if we're going to be in the Computer Science department, can we
> get away from the idea of "logic as a regimentation of natural
> language" (which is fine for the Philosophy department) and move to
> the idea of logic as equations of Binary Artihmetic and Boolean
> Algebra?

Hi, about this point: perhaps it is helpful to recall some very basic
stuff, put in very simple terms, even if it may sound quite
elementary...

While what (I think) you call boolean logic may be useful for explaining
(basic) computing operations, and provide an adequate foundation for
(basic) hardware design, it just does not scale up to higher levels of
abstraction, as needed to talk and reason about complex computing
systems.

It really takes quite a bit to build up from bit-level operations as
actually performed by the hardware up to concepts such as "ADTs",
"algorithms", "objects", "functions", "modules", "types", "abstract
machines" - ideas such as "code as data", "atomicity", "fairness",
"levels of interpretation" - and all the great stuff that belong to
the world of (both practical and theoretical) computer science. To be
able to talk about all this we need much more than basic "binary
artihmetic and boolean algebra".

For our purposes, it is perhaps more convenient to think of "symbolic
logic" as just a the convenient language to describe properties and
formally reason about objects in some domain.

Currently, one single unified logic is not yet available, we need
several logics;
different logics describe different kinds of properties of CS objects,
useful for different purposes, all based, we hope, on a common trunk
of deep principles.

For example, I guess every programmer appreciate the usefulness of
types in programming languages. But a type system is nothing more than
a certain kind of a symbolic logic. It does not calculate with
concrete data values or bits, but instead uses logic to deduce and
reason about the type of things around, allowing the compiler to
prove, at compile time, without executing the generated code, that a
program satisfies a set of properties. Namely that, when actually
executed, it will not suffer from basic runtime errors, such as
invalid operations on data, etc.

This is just an example. Each particular logic provides reasoning
rules, allowing us to know how properties expressible in the logic
relate, and how the objects the logic talks about satisfies a property
or not. In some cases, algorithms can be provided to check whether an
object satisfy a given property (automated verification).

These basic concepts are essential for computer science, as no
artifact (processors, algorithms, programming languages, compilers,
etc) can be precisely and fully understood without reference to the
various properties it should satisfy. If you want to check that a
given code piece really returns a sorted vector, you cannot do this
conveniently just with (what I think you call) boolean logic (even if some
simple verification problems can be "compiled" down to boolean
logic). As another example, some of us may teach (separation) logic to
students to empower them with solid techniques for checking the
absence of races in concurrent java programs. As yet another example,
we (with colleagues) have recently discovered how to use (linear)
logic to reason about the safety of session protocols in distributed
systems.

So there is this idea that (symbolic) logic is actually the "calculus
of computer science" (see
e.g. http://www.cs.rice.edu/~vardi/logic/). While symbolic logic has
roots in philosophy, I guess it is fair to recognize that it is being
now developed mostly in conection with (theoretical) computer science
and math, often driven by the deep relation between logic and
computation. So I would really encourage you to look into all this.

Logical concepts may be also perhaps useful to discuss other issues in
this thread such as "specs versus programs", and "declarative versus
imperative".  Let me copy some remarks by Hoare (ACM, 2009):

"So I believe there is now a better scope than ever for pure research
in computer science. The research must be motivated by curiosity about
the fundamental principles of computer programming, and the desire to
answer the basic questions common to all branches of science: what
does this program do; how does it work; why does it work; and what is
the evidence for believing the answers to all these questions? We know
in principle how to answer them. It is the specifications that
describes what a program does; it is assertions and other internal
interface contracts between component modules that explain how it
works; it is programming language semantics that explains why it
works; and it is mathematical and logical proof, nowadays constructed
and checked by computer, that ensures mutual consistency of
specifications, interfaces, programs, and their implementations."

So I guess this view of logic actually belongs to the CSD ...

Thanks,

Luis

-- 
Best regards,
Luis Caires
http://ctp.di.fct.unl.pt/~lcaires/
Departamento de Informática
FCT Universidade Nova de Lisboa