Kathi Fisler Position Statement

Formal methods education should address how to identify, develop, and prove formal statements --- in particular, theorems --- about programs and systems. This encompasses activities ranging from type-checking (where the theorem is stated implicitly and proved automatically) to model-checking (theorem stated explicitly and proved automatically) to theorem-proving (theorem stated explicitly and proved manually). It should also include activities generally excluded from formal methods, but that rely on or yield such theorems. For example, running a compiler optimization relies on a theorem that ensures the preservation of correctness, while simulating a design yields a (rather weak) theorem about the design relative to particular input sequences.

Students at all levels should be encouraged to think about the theorems associated with computer science. In particular, a student should be able to answer the following questions:

  1. What kinds of formal statements can be made about a system?
  2. When is a formal statement about a system provable?
  3. When is a formal statement about a system useful?
  4. What resources are needed to prove a given formal statement?
  5. What tools and techniques exist for validating formal statements about systems?

Our recommendations for formal methods education should propose ideas that develop students' skills in addressing these questions. I believe general formal methods education should be integrated into existing undergraduate and beginning graduate courses. The answers to all but the second and fourth questions posed above depend on the application area. At a minimum, computer science courses should discuss the types of formal statements about systems that are relevant to their area. Where appropriate, students should also learn how to prove such statements. In an operating systems course, this would take the form of protocol verification using model checking. A compilers course should discuss how to derive compilers from language specifications and how to establish the correctness of optimizations. Programming languages courses should cover resource safety. In short, there are numerous examples of how formal methods issues arise in existing courses if we can find ways to encourage our colleagues to discuss them.

A thorough formal methods program must also go beyond covering issues piecemeal in existing courses. A separate graduate level course should address the relationships between the techniques seen through existing courses. Rather than focusing on formal methods, however, this course should emphasize proof techniques, their relationships, and the theoretical issues governing their use. This course would be distinct from general courses in applied logic because of its particular focus on proofs. Such a focus is sufficiently general to make the course useful to students outside of formal methods, while still covering the key ideas appearing in formal methods. A combination of this course and the practical insights gained from using formal methods in lower level courses would provide a solid and well-rounded formal methods education.