Monday, Wednesday, Friday: 10:30 - 11:20
Office Hours: Tuesday, Thursday: 3–4pm
Office Hours: Monday: 12–1pm
More generally, these questions broadly fall under the term formal methods, an important branch of computer science that looks to mathematics (specifically, logic) to help us (at least in this class) precisely reason about programming language features and behaviors. Our focus will be to explore core ideas in programming languages from a rigorous, foundational, and principled perspective enabled by couching programming language concepts and the vocabulary we use to reason about them in terms of well-defined mathematical objects (e.g., sets, functions, relations) and associated reasoning strategies (e.g., induction). To do so, we will undertake our study using small language definitions (program calcuii), sufficiently expressive to serve as a useful object of study, but not burdened with features that while perhaps necessary for real-world implementations, are semantically uninteresting.
The course will be centered around the use of tools (proof assistants, model checkers, type systems) that enable better understanding of how we might design, specify, and implement language features. We will also use these tools to help us think about how to gain stronger assurance and confidence that the programs we write do what we expect them to do.
From the above description, you can conclude that this course will not be a survey of existing languages or a taxonomy of language constructs. Neither will it be a course on programming or software engineeringper se. Instead, the course will be structured to allow us to explore new ways to understand programming languages generally that help us to answer questions such as the following:
To help answer these questions, the course is designed around several interleaved themes: (1) the role of logic and related mathematical formalisms in programming language specification and design; (2) formal reasoning devices that precisely explain the meaning of programming language features and program executions; (3) the use of types to define and specify safety conditions on program executions, and to enrich language expressivity; (4) characterization of different notions of correctness and development of mechanisms to verify that programs are correct with respect to their specification; (5) the use of automated tools (e.g., proof assistants, program verifiers) to help validate important theorems that describe useful properties based on the structure of (2) and (3), using techniques enabled by (1).
By the end of the class, students should be comfortable with objectively assessing and comparing superficially disparate language features, understanding how these features impact implementations, be able to distinguish concepts that are truly foundational from those that just appear to be, and be able to critically reason about program correctness and safety. Most importantly, the overarching goal of this course is to equip students to ask better questions about language design, even if the answers themselves are not readily apparent.
It is assumed that students taking this class would have had exposure to an undergraduate software engineering and/or compilers class, and be comfortable with basic mathematical concepts, and software implementation techniques. There will be a number of programming exercises in the class, but no prior background in any specific programming language is necessary.
Students are encouraged to work together to clarify issues presented in class. However, students are not allowed to collaborate on programming assignments or examinations.
Grading for the class is as follows:
A pair of scribes will be appointed for every topic, which may span two to three classes. The role of the scribes is to summarize and clarify the lectures, and transcribe this summary into a form suitable for posting on the course web-site. Scribes will be expected to research the topic beyond what is discussed in lecture; an implicit goal of this class is to foster intellectual creativity and curiosity and to improve communication and exposition skills - the scribe process gives students an opportunity to explore a topic in greater depth and to share their understanding with other members of the class.
There will also be a number of homework assignments given throughout the semester; these will typically be due two weeks after posting.
We will use the online textbook Software Foundations, available here for part of the course. Students should download the text, and install the Coq mechanized proof assistant (see here).
In fact, the textbook is essentially one large Coq program, with explanation provided in comments, so students are encouraged to bring their laptops to class to interactively explore the material along with the instructor.
In addition, students might find the following texts also useful:
Specifications, Semantics, and Verification