Alexander Kurz

Logic in Computer Science

Compared to other disciplines such as physics and engineering, computer science is still a young field. With the amazing technical advances we have seen, it is not a surprise that we still need to develop the computer science mathematics that will adequately support the engineering of secure and reliable software.

As a first rough approximation, one may say that logic is to computer science what mathematics is to physics.

Conversely, computer science is having an huge influence on research in logic. I didn’t try to count for myself, but I think it is safe to say that the vast majority of logicians nowadays is employed in computer science departments. By the way, one of them co-authored the graphical novel Logicomix in which Bertrand Russell and the history of logic are the main protagonists.

The best known applications of logic to computer science are probably still in hardware design (digital circuits), since Shannon’s Symbolic Analysis of Relay and Switching Circuits from 1937.

Current research in logic is driven more by applications to programming and software engineering. These applications led us from the one universal logic which Russell was still seeking at the beginning of the 20th century to a large zoo of bespoke logics, each with its own applications and algorithms.

The reason why we need so many logics is in its essence contained in Turing’s famous result that the so-called halting problem cannot be solved by an algorithm, or, in more technical terms, it is undecidable. In fact, a corollary of the unsolvability of the halting problem is Rice’s theorem saying that all non-trivial semantic properties of programs are undecidable.

To deal with the undecidability, several strategies have been employed:

This line of research has been very successful and gave rise to a wide range of logics and software tools, many of which are nowadays mature enough so that they can be used by programmers who did not specialise in logic.

Logic Area Example Tool  
  propositional logic SAT-solving MiniSat
  temporal logic model checking SPIN
  Hoare logic static program analysis Dafny
  first-order logic data base query languages SQL
  logic programming Prolog
  automated theorem proving Vampire
  type theory interactive theorem proving Lean

Each of these logics comes in many variations. Each of this areas are big enough to spend a life-time of research in it. I would expect a student who takes a course on logic in computer science to know about SQL and maybe Prolog. But all of these tools are worth knowing.