Does Every Computer Scientist Need to Know Formal Methods?

By Manfred Broy, Achim D. Brucker, Alessandro Fantechi, Mario Gleirscher, Klaus Havelund, Markus Kuppe, Alexandra Mendes, André Platzer, Jan Oliver Ringert, and Allison Sullivan.

We focus on the integration of Formal Methods as mandatory theme in any Computer Science University curriculum. In particular, when considering the ACM Curriculum for Computer Science, the inclusion of Formal Methods as a mandatory Knowledge Area needs arguing for why and how does every computer science graduate benefit from such knowledge. We do not agree with the sentence "While there is a belief that formal methods are important and they are growing in importance, we cannot state that every computer science graduate will need to use formal methods in their career." We argue that formal methods are and have to be an integral part of every computer science curriculum. 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. The same way, students have to understand why and how methods work, what their formal background is, and how they are justified. No engineer should be ignorant of the foundations of their subject and the formal methods based on these.

In this paper, we aim to highlight why every computer scientist needs to be familiar with formal methods. We argue that education in formal methods plays a key role by shaping students’ programming mindset, fostering an appreciation for underlying principles, and encouraging the practice of thoughtful program design and justification, rather than simply writing programs without reflection and deeper understanding. Since integrating formal methods into the computer science curriculum is not a straightforward process, we explore the additional question: what are the trade-offs between one dedicated knowledge area of formal methods in a computer science curriculum versus having formal methods scattered across all knowledge areas? Solving problems while designing software and software-intensive systems demands an understanding of what is required, followed by a specification and formalizing a solution in a programming language. How to do this systematically and correctly on solid grounds is exactly the supported by Formal Methods.

Keywords:
Formal methods, software and systems engineering, computer science university curriculum

Please cite this work as follows:
M. Broy et al., “Does every computer scientist need to know formal methods?” Formal Aspects of Computing (FAC), 2025, doi: 10.1145/3670795. Author copy: http://logicalhacking.com/publications/broy.ea-fm-in-cs-education-2025/

BibTeX
@Article{ broy.ea:fm-in-cs-education:2025,
  author    = {Manfred Broy and Achim D. Brucker and Alessandro Fantechi and
               Mario Gleirscher and Klaus Havelund and Markus Kuppe and
               Alexandra Mendes and Andr{\'e} Platzer and Jan Oliver Ringert
               and Allison Sullivan},
  journal   = {Formal Aspects of Computing (FAC)},
  language  = {USenglish},
  title     = {Does Every Computer Scientist Need to Know Formal Methods?},
  year      = {2025},
  issn      = {0934-5043},
  publisher = {Association for Computing Machinery},
  address   = {New York, NY, USA},
  pages     = {},
  volume    = {},
  number    = {},
  areas     = {formal methods, pedagogy},
  doi       = {10.1145/3670795},
  keywords  = {Formal methods, software and systems engineering, computer
               science university curriculum},
  abstract  = {We focus on the integration of Formal Methods as mandatory
               theme in any Computer Science University curriculum. In
               particular, when considering the ACM Curriculum for Computer
               Science, the inclusion of Formal Methods as a mandatory
               Knowledge Area needs arguing for why and how does every
               computer science graduate benefit from such knowledge. We do
               not agree with the sentence "While there is a belief that
               formal methods are important and they are growing in
               importance, we cannot state that every computer science
               graduate will need to use formal methods in their career." We
               argue that formal methods are and have to be an integral part
               of every computer science curriculum. 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.
               The same way, students have to understand why and how methods
               work, what their formal background is, and how they are
               justified. No engineer should be ignorant of the foundations
               of their subject and the formal methods based on these.
               
               In this paper, we aim to highlight why every computer
               scientist needs to be familiar with formal methods. We argue
               that education in formal methods plays a key role by shaping
               students' programming mindset, fostering an appreciation for
               underlying principles, and encouraging the practice of
               thoughtful program design and justification, rather than
               simply writing programs without reflection and deeper
               understanding. Since integrating formal methods into the
               computer science curriculum is not a straightforward process,
               we explore the additional question: what are the trade-offs
               between one dedicated knowledge area of formal methods in a
               computer science curriculum versus having formal methods
               scattered across all knowledge areas? Solving problems while
               designing software and software-intensive systems demands an
               understanding of what is required, followed by a specification
               and formalizing a solution in a programming language. How to
               do this systematically and correctly on solid grounds is
               exactly the supported by Formal Methods.},
  pdf       = {},
  note      = {Author copy: \url{http://logicalhacking.com/publications/broy.ea-fm-in-cs-education-2025/}},
}