Education and Knowledge Transfer
Our experience using Coq in the classroom has convinced us that interactive theorem provers provide a uniquely tangible way for students to learn how to deal with mathematical topics such as reading and writing specifications. The instantaneous and interactive feedback students get about the steps they make while struggling with a proof, along with the positive reinforcement of “solving a goal,” yields an engaging environment for learning. Moreover, because using an interactive theorem prover often feels like “just programming,” the mathematics connects with students in a way that is more concrete than in traditional pen-and-paper approaches.
As part of this Expedition, we are working to develop course modules and software projects that instructors can incorporate into standard, well-understood slots in the undergraduate curriculum. These modules will be based on rigorously specified and validated interfaces that will be usable in traditional courses, so they will be accessible to students and instructors who may wish to approach them less formally. Moreover, the underlying formal specifications will permit enrichment exercises and additional course modules where students explicitly work with formal specification and verification.
Our overall goal is to catalyze the adoption of deep specification techniques through a tightly integrated combination of focused research, course development, and community building. The diagram above visualizes these activities and their connections. We will study both industrial-scale systems (the outer wheel, connecting to the broader world) and simplified educational versions (the inner wheel, connecting to the traditional curriculum).
Improved compilers and OS courses
We are developing new curricula for undergraduate courses in compilers and operating systems. A traditional compilers course has implementation projects that, phase by phase, translate a fragment of source to assembly language via intermediate representations. A contemporary (but still traditional) course might use the LLVM intermediate representation. Our deep-specification version of this course will follow a similar structure, except that each language (source, LLVM IR, and assembly) would also be defined by formal specifications for a carefully chosen subset of the full versions of those languages used in practice. Such supplemental formal specifications will provide a precise description of the language semantics, which will be informative for the students doing the projects. Moreover, instructors will benefit from tools, such as testing harnesses, that use the specifications for test-case generation or validation of the students' implementations; even mathematically unsophisticated students can, for example, apply property-based random testing tools to their code and thereby learn the practical value of good specifications. In addition, we are developing formal project material in which the students can learn how to prove the correctness of (an instance of) the project compiler; see “Formal methods in systems,” below.
We are also developing an operating systems course with an implementation project. Many students shy away from traditional OS classes because low-level kernel debugging is time-consuming and challenging. Although the very purpose of an OS kernel is to build layers of abstractions over hardware resources, kernel components (even in an instructional OS) are almost always tangled together with subtle interdependencies. A deeply specified version of an OS course will organize the lab work around (a stripped down pedagogical version of) the CertiKOS kernel. We will provide the students a fine-grained decomposition of all key kernel functionalities, with complete specifications for all of these layers. Students can implement new modules at any of the verified abstraction layers. This will save debugging time and provide students a deeper understanding about the essence of many kernel mechanisms.
We expect that the compilers and OS courses will be accessible to instructors and students at the undergraduate level at any university. The deep specifications are not “intrusive”: they are used as conceptual tools, while implementations are done in conventional languages.
Formal methods in systems
Our compilers and operating-systems courses are both based on projects in which students program against deep-specification interfaces. In both cases there are “instructors' solutions” that are fully formally verified. In the basic courses (described above), the specifications help students with understanding, but the students won't learn how to do mechanized formal verification.
We are also developing an advanced course on systems verification that uses the same verified compiler and OS as pedagogical examples. The focus in this course will be on reasoning about deep specifications of compilers and OS kernels in Coq, including the verification of implementations (in Coq and in C, respectively). This course will have a few weeks of introductory material on logic and proof in Coq, and then it will cover the LLVM-based and CertiCoq-based material that students (may) have seen in our compilers and OS “systems” courses.
At many universities, instructors may be ill-prepared to teach this material without significant support. We aim to provide that support. We are building the “Systems Verification in Coq” course as a MOOC so that instructors anywhere can learn and teach this material. We will also unbundle the components of this MOOC: “ textbook,” online exercises, and video modularized, so that instructors can use the videos or not. Instructors will also be able to select from intro, compilers, and OS components. At some universities, instructors may be able to fit advanced verification material into our basic compilers or operating-systems courses instead of as a separate course, and the MOOC will be modular enough to permit that.
Course Infrastructure for deep specifications
Many computer science educators recognize the importance of rigorous mathematical training as a key ingredient that separates computer science from mere vocational training in programming. Rigorous mathematics requires rigorous proofs. Unfortunately, the state of the art is to rely on teaching assistants to grade problem sets and give feedback by holding office hours; when it comes to teaching rigorous proofs, these methods are hard to scale, even to classes of a few dozen students, much less hundreds, thousands, or more. Deep specification, together with interactive theorem proving tools, addresses this problem. Creating deeply specified versions of various kinds of course material would allow us to develop tools capable of automatically grading formal proofs and conveying effective feedback to students.
We are developing a software platform for creating interactive online texts in computer science and mathematics, which intersperses text and exercises using tools based in formal logic, including interactive proof assistants, automatic constraint solvers, and testing tools. The greatest challenge here will be in designing sufficiently intuitive interfaces for constructing formal proofs and getting feedback on mistakes in them. We believe this sort of interface can have a transformative effect, moving us toward a world where every computer science graduate knows, for example, how to carry out a convincing proof by induction. This kind of learning can scale to very large numbers of students—even MOOC scale—with minimal course staffing, by taking advantage of tools for mechanized proof checking to give instant feedback.
Our starting point for the model of how to present the Coq-based components of such material is the Software Foundations text by Pierce et al., already in use in graduate-level courses at our institutions and elsewhere.
Propagating deep specifications into industry
Industrial application relies on good tools, good documentatation and training materials, and open-source prototypes of realistic systems. Developing these course materials will serve several purposes. By incorporating, pedagogical versions of the large-scale systems that we use to conduct the deep specification research, it will serve as tests of our research specifications at a smaller scale. Targeting undergraduate courses will force us to apply the highest standards of usability in evaluating the tools we build and the system specifications we create. Exercising both the specifications and the tools in this way will help with the process of transitioning to industrial applications.