---
tags: chapman, programming langauges, logic, Peter O'Hearn, byron cook, moshe vardi,
---
# Logic in Computer Science

Compared to other disciplines such as mathematics and physics, 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.

## Background

As a first approximation, one may say that the [ "unreasonable effectiveness" of mathematics in physics](https://www.maths.ed.ac.uk/~v1ranick/papers/wigner.pdf) is paralleled by an ["unreasonable effectiveness" of logic in computer science](https://www.cs.rice.edu/~vardi/papers/aaas99.jsl.pdf).

Conversely, computer science is having a huge influence on logic. The vast majority of logicians nowadays are employed in computer science departments. By the way, one of them co-authored the graphical novel [Logicomix](https://www.logicomix.com/en/index.html) in which Bertrand Russell and the history of logic are the main protagonists (highly recommended).

The best known applications of logic to computer science are probably still in hardware design (digital circuits), dating back to Shannon's [Symbolic Analysis of Relay and Switching Circuits](https://en.wikipedia.org/wiki/A_Symbolic_Analysis_of_Relay_and_Switching_Circuits) from 1937.

But 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](https://en.wikipedia.org/wiki/Halting_problem) cannot be solved by an algorithm, or, in more technical terms, is *undecidable*. In fact, a corollary of the unsolvability of the halting problem is [Rice's theorem](https://en.wikipedia.org/wiki/Rice%27s_theorem) saying that all non-trivial semantic properties of programs are undecidable.

To deal with this undecidability, several strategies have been employed:
- Design bespoke decidable logics that work on abstract models instead of on general programs.
- Build interactive tools that react to guidance by an expert instead of being fully automated.
- Develop approximate methods that find a very good answer with a high probability.

## Successes of Applied Logic

Applied logic as an effort to deal with the undecidability of all interesting problems in computing 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.

The following table gives a rough and incomplete overview.

**Examples of Logics, Research Areas and Software Tools:**

| Logic | Research Area | Tools |
|:---:|:---:|:---:|
|[propositional logic](https://en.wikipedia.org/wiki/Propositional_calculus) | [SAT-solving](https://en.wikipedia.org/wiki/Boolean_satisfiability_problem#Online_SAT_solvers) | [MiniSat](https://www.msoos.org/2013/09/minisat-in-your-browser/) |
|[temporal logic](https://en.wikipedia.org/wiki/Temporal_logic) | [model checking](https://en.wikipedia.org/wiki/Model_checking) | [SPIN](https://en.wikipedia.org/wiki/SPIN_model_checker) |
| [Hoare logic](https://en.wikipedia.org/wiki/Hoare_logic) | [static program analysis](https://en.wikipedia.org/wiki/Static_program_analysis) | [Dafny](https://en.wikipedia.org/wiki/Dafny) |
| [description logic](https://en.wikipedia.org/wiki/Description_logic) | [knowledge representation](https://en.wikipedia.org/wiki/Knowledge_representation_and_reasoning) | [OWL](https://en.wikipedia.org/wiki/Web_Ontology_Language) |
| [first-order logic](https://en.wikipedia.org/wiki/First-order_logic) | [data base query languages](https://en.wikipedia.org/wiki/Query_language) | [SQL](https://en.wikipedia.org/wiki/SQL) |
| " | [logic programming](https://en.wikipedia.org/wiki/Logic_programming) | [Prolog](https://en.wikipedia.org/wiki/Prolog) |
| " | [automated theorem proving](https://en.wikipedia.org/wiki/Automated_theorem_proving) | [Vampire](https://en.wikipedia.org/wiki/Vampire_(theorem_prover)) |
| [type theory](https://en.wikipedia.org/wiki/Higher-order_logic) | [interactive theorem proving](https://en.wikipedia.org/wiki/Type_theory) | [Lean](https://en.wikipedia.org/wiki/Lean_(proof_assistant)) |

Each of these logics comes in many variations, many of which fall under the broader umbrella of [modal logic](), a beautiful and thriving research area in its own right. Each of these areas is 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 and OWL. But all of these tools are worth knowing. And all of them are based on implementing some kind of **logical reasoning**.

If you are a student at Chapman with an interest in logic, let me know. For example, I'd be more than happy to teach a course about (a subset of) the table above. There is also the possibility to do a project, for example on how to use one of the tools above in order to solve a practical problem of interest. If you are a maths student, there are also purely theoretical problems to consider.

## Applications of Formal Methods in Industry

Two theoretical computer scientists who are leading industrial applications of formal methods are Peter O'Hearn and Byron Cook. I collect here some links to check out.

- Facebook (Peter O'Hearn):
- [Facebook's Code Checker](https://www.youtube.com/watch?v=tKR2UZdRpV0)
- [Continuous Reasoning: Scaling the impact of formal methods](https://www.youtube.com/watch?v=HW5Zq1TsQqU)
- [Scaling Static Analyses at Facebook](https://dl.acm.org/doi/pdf/10.1145/3338112)
- [Applying Formal Verification to Microkernel IPC at Meta](https://www.cs.cornell.edu/~noamz/files/pubs/cpp22.pdf)
- [Finding Real Bugs in Big Programs with Incorrectness Logic](http://www0.cs.ucl.ac.uk/staff/p.ohearn/RealBigDraft.pdf)
- Amazon (Byron Cook):
- [On the Business of Proof ](https://www.youtube.com/watch?v=g-DH_b5bFd4)
- [Formal Reasoning about the Security of Amazon Web Services](https://www.youtube.com/watch?v=JfjLKBO27nw)

## Summary

We can distinguish two levels of applications of logic in computer science. Theoretical applications and practical applications.

Theoretical applications of logic are in building models of computation. Examples include digital circuits for hardware, memory models, models of concurrency and distributed computing, etc

Practical applications of logic come via hardware and software designed by engineers based on these models of computation. All of our IT infrastructure can be taken as an example.

But, of course, we as logicians dont want to only brag about past achievements ... so there is a lot of research to do ...

## More ...

One of the leading logicians of our times, [Moshe Vardi](https://scholar.google.com/citations?user=DQaARsgAAAAJ), has a number of talks that are related to logic but branch out to a variety of topics in computer science and beyond.

- The two lectures [From Aristotle to the iPhone](https://www.youtube.com/watch?v=wOQuW6QFdos) and [From Greek Paradoxes to Political Paradoxes](https://logicday.vcla.at/vienna-logic-day-lecture/) have some overlap. The first has more on the history and the second more on how modern communication technology is changing our society.
- [Program Verification: a 70-Year History](https://www.youtube.com/watch?v=HJkukhoQFzo&t=590s).
- [Humans, Machines, and Work: The Future is Now](https://www.youtube.com/watch?v=5ThiClGEBes) is about automation and the future of work. Takeaways:[^moretakeaways] Job polarization (46:00) and its possible causes (52:24). The main thrust of his argument is that automation has already taken many jobs and AI will certainly not slow this trend down.
- [Ethics Washing in AI](https://www.youtube.com/watch?v=qW9WFOosaWc), June 23, 2022.

[^moretakeaways]: The talk presents data on many topics: GDP vs Jobs in Manufacturing; Manufacturing Output per Worker; The Great Coupling (Productivity, GDP, Employment, Income) until 1985 and the Great Decoupling after that; Growing Inequality; Inequality vs Social Mobility; Labor-Force Particiation by Occupation; Labor Share of National Income; Job Polarization; Education.