[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
On Fri, May 3, 2013 at 11:28 PM, Mark Janssen <[email protected]> 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
