FME’s Teaching Committee has recently organised a special issue of Formal Aspects of Computing that puts forward different perspectives on why and how Formal Methods should be represented in Computer Science curricula. The discussion was triggered by the guidelines that ACM has been publishing for computer technology university curricula for more than five decades.
A summar article of the discussed perspectives appeared in the December 2024 issue of ACM Inroads: The Role of Formal Methods in Computer Science Education.
ACM CS Curricula Guidelines
ACM has been publishing guidelines for computer technology university curricula for more than five decades, with the first one specifically for Computer Science published in 2001. To the best of our knowledge, these are the only curricular guidelines that have worldwide recognition. While it is likely that no university follows them to the letter, they are enormously valuable as a reference point. Since the field of computer technology evolves quickly, ACM regularly updates its guidelines on what should be taught. For instance, the Computer Science curricular guidelines are revised once every decade; CS2023 is the latest revision, recently published. The ACM teaching recommendation model is complex. In short, it contains 17 knowledge areas deemed essential for Computer Science. Each such area further divided into knowledge units made of topics, some topics mandatory to teach and some elective.
Should Formal Methods be part of CS Curricula?
The special issue of Formal Aspects of Computing puts forward different perspectives on why and how Formal Methods should be represented in Computer Science curricula, in some cases, just as suggested in the ACM guidelines, but in other cases, providing different guidance. The starting point is the questions below, which have arisen from informal discussions with CS2023 contributors to various knowledge areas.
The 35 authors of the papers in the special issue have extensive experience in teaching Formal Methods in Academia or working with them in Industry. They argue for introducing Formal Methods as a knowledge area in the ACM guidelines, since currently Formal Methods are covered only as elective topics in some knowledge units in two distinct knowledge areas: Foundations of Programming Languages and Software Engineering.
Formal Methods are supported nowadays by efficient software tools; this is a game changer regarding their usability and adoption from students and practitioners. The evidence put forward in the papers of the special issue suggests that not indicating Formal Methods as a core domain in a Computer Science curriculum in 2024 is incomprehensible, similar maybe to how Artificial Intelligence was not included just 10 years ago in the 2013 guidelines.
- Does every Computer Scientist need to know Formal Methods?
Broy et al. argue why every Computer Scientist needs to know the theoretical background of their field. An analogy is given to database management: “Just as not all graduates will need to know how to work with databases either, it is still important for students to have a basic understanding of how data is stored and managed efficiently.’’ Their message brings out the fact that Computer Science graduates are also (software and systems) engineers. And it is perhaps uncontroversial that “No engineer should be ignorant of the foundations of their subject and the formal methods based on these.’’ The paper is available here.
- Are Formal Methods just for the safety-critical industry?
ter Beek at al. present an extensive review of industrial uses of Formal Methods, demonstrating that safety-critical systems are not the only beneficiaries of precision, reasoning, and proof. The authors “… present a broad scope of successful applications of formal methods in industry, not limited to the well-known success stories from the safety-critical domain”. For example, they present use cases in lithography manufacturing and cloud security in e-commerce, and industrial use in Europe, Asia, and North and South America. The paper is available here.
- Is the current offer of Formal Methods education adequate?
Dongol at al. explain that Formal Methods are currently not taught well, being often associated with logic and theory. They argue that we need to teach all Computer Science students “Formal Methods thinking’’, which they define as the ideas from Formal Methods applied in “informal, lightweight, practical and accessible ways’’. This includes, for instance, understanding key concepts, but applying them using natural languages. The authors argue that Formal Methods thinking should be part of the recommended curriculum for every Computer Science student, since students then become much better programmers. The paper is available here.
A one-page summary of the contributions of the papers appears in the CS2023 curricular guidelines on page 433.
For more information, see the website of FME’s Teaching Committee.