Logic & Computation

Meeting Times

Lectures will not be recorded, though lecture notes will be posted after class (see Schedule).

Course Staff / Office Hours

Calendar of Virtual Office Hours, held via Teams using Khoury Office Hours App.

Non-virtual hours held by Daniel Patterson, Raisa Bhuiyan, Ryan Jung, Lucy Liu, Yuhao Zhou (see below). For most up to date virtual hours, consult calendar linked above!

In Fundamentals 1, you learned about the systematic design of software. You learned how to take a problem statement and refine it into functioning software in a step-by-step process called the Design Recipe. This iterative process allowed you first to discover the relevant data, then identify the operations on that data needed to perform the task, express your understanding of the problem in tests, and finally implement the code. In Discrete Structures, you learned, among other things, about propositional and first-order logic, and how to express, reason about, and prove mathematical statements. The goal of this course is to combine these two: to apply logic to enable reasoning about programs. Why do we care?

Even only programming for one semester, only writing programs that stretched into the hundreds of lines, you certainly wrote programs with bugs in them. Most you probably caught, some your TAs may have caught, and the odd bug may have slipped through. Creating bugs in software doesn’t stop with experience, and certainly doesn’t disappear "naturally" — indeed, much of the field of software engineering, developed over more than a half-century has been focused around developing processes to try to reduce the number of bugs in software. You may take a software development or software engineering class here, and both will cover human processes that can help increase the reliability and reduce the number of bugs in the software you write. While that is incredibly valuable, it’s not the only approach.

Running parallel to that is another field, formal methods, which took a different tactic: rather than developing human processes, or particular development strategies, the goal was to use logic and math to increase the trustworthiness of software in a quantifiable way. Most of this work originated within the national security apparatus of the US Government, but eventually, it spread to other domains.

Indeed, software that runs fly-by-wire control systems in airplanes, or control systems in modern cars, is software where bugs can directly lead to loss of life. And if those examples don’t feel compelling, realize there is software controlling the administration of electricity directly to cardiac tissue in pacemakers, delivering radiation doses in hospitals, or insulin doses via insulin pumps. Of course, there are plenty of places where bugs can have significant consequences that fall short of directly threatening human life: within the past few decades, most financial transactions have moved mostly or wholely online, so that bugs can lead to catastrophic financial costs, nevermind a whole host of other problems. Some of you may be cybersecurity majors: much of the work of security is trying to figure out exactly how systems can work, so that malicious actors can’t use them in unintended ways.