Although on many occasions, especially at FM conferences, highlights of the use of Formal Methods in software development are presented, FM plays just a minor role in both the everyday work of software engineers as well as Computer Science and Software Engineering curricula. To me, one of the main reasons for the status quo is that mathematics education, as it is usually done today, does not enable students to understand and to use Formal Methods. Software engineering is a young engineering discipline that is di erent in many respects from the classical engineering elds. To me the most distinguishing point is the kind of mathematics that serves the respective elds well. Classical, calculus-based engineering mathematics is of no use. Just putting more emphasis on Discrete Mathematics, as recommended and usually done, is { by far { not enough. I will report on an alternative approach to teaching introductory mathematics to students of CS and SE which started already in the 1980s. The whole rst year is dedicated to teach "The Language and Methods of Mathematics". It is also an introduction into FM, i.e. in the second semester students learn to do Hoare-style correctness proofs, for example. Implementing such radical changes in the curriculum is, of course, also a "political" problem. Some of these aspects will be discussed, for example that this will be possible only if SE is regarded a discipline of its own, not just a part of CS. In many cases it will also be necessary to take math education away from math departments. Real (IR -) mathematicians have a hard time understanding the mathematical needs of software engineers. In the last section I will present some personal thoughts about which advanced mathematical topics could play a major role in future SE education, as for example (partial) di erential equations do in classical engineering mathematics. For me, these topics come from algebra, aiming at "conceptual mathematics", which essentially is category theory.
Although on many occasions, especially at FM conferences, highlights of the use of Formal Methods in software development are presented, FM plays just a minor role in both the everyday work of software engineers as well as Computer Science and Software Engineering curricula.
There are reasons to believe that this cannot be changed dramatically, or even that it should not be changed. Many practitioners regard FM as not applicable and thus unimportant for the main stream, relevant just in some niches. I assume that most participants of a workshop on FM in SE education will disagree. So, what can we do to bring FM closer to the main stream in software development?
To me, one of the main reasons for the status quo is that mathematics education, as it is usually done today, does not enable students to understand and to use Formal Methods. This seems a bit remote, at rst glance. In this paper, which is no research paper proper, but more an extended position statement, I will try to explain my point of view and give recommendations for how to make FM more popular. 2
It is generally agreed that mathematics plays an important role in the curriculum of the classical engineering disciplines like Civil, Mechanical or Electrical Engineering. Often up to 30% of an engineers education is devoted to mathematics. The mathematics taught there is well-established, almost exclusively calculus-based, since the advent of computers numerical mathematics plays an important role as well.
Software Engineering is a young engineering discipline that is di erent in many respects from the classical engineering elds. To me the most distinguishing point is the kind of mathematics that serves the respective elds well. Classical, calculus-based engineering mathematics is of no use. Just putting more emphasis on Discrete Mathematics, as recommended and usually done, is { by far { not enough.
There is a lot of material, mostly developed by high-ranking committees of
IEEE Computer Society and ACM, giving guidelines for CS and SE curricula
both at the undergraduate and the graduate level or describing the "body of
knowledge" in the respective elds. All of that is valuable and great, I just
criticize one point: the attitude towards mathematics. Let's start with SE2004
([
It seems that everybody is { more or less { satis ed with this kind of math
teaching. In our community as well I rarely hear complaints that students are
not prepared for Formals Methods in introductory math courses although FM
is nothing else than software development strictly based on mathematics. Many
practitioners (and academics) regard FM, as already said in the introduction,
as not applicable and thus unimportant. This is di erent from the classical
engineering disciplines. As Peter Henderson put it in [
It is pretty clear which basic mathematical topics are important for Formal
Methods, an early book covering this is [
My view on a proper, realistic mathematics education for software engineers is
perhaps characterized best by part of the title of a talk I gave in 2002 at a
conference on teaching mathematics: "It Should Be Radically Di erent!" That
is di erent from math for the classical engineering disciplines, and thus di erent
from how it is taught at most places today. In [
The paper is more than ten years old and I probably would use di erent examples and other wording today. There I use the example of de ning the notion of "abstract data type" mathematically, i.e. via algebraic speci cation, to show that a di erent type of math is needed than classical, calculus-based engineering math.
For more than 30 years we have been teaching introductory mathematics to
students of Computer Science (called "Informatik", at Johannes Kepler
University, Linz, Austria) and of Software Engineering (at the University of Applied
Sciences Upper Austria) in a di erent way. Unfortunately the textbook we used
([
Although there is a lot more to be said about our approach, in this writing I simply want to underscore two topics that are dear to me: specifying and proving.
What is the most important thing that one has to teach to SE students from the beginning? Teach them to specify, then to specify, and once again { to specify! In our introductory math course students have to write their rst formal problem speci cation after four weeks. You just need the basic language of mathematics for that, i.e., propositional and predicate logic. But you need much more time to explain the details than is usually allocated for these topics in introductory math courses for CS. Mathematicians regard this use of logic as trivial, and in textbooks on discrete math it's usually worth just a few pages. Speci cation means translating natural language into the (formal) language of mathematics, but also the other direction is important: learning to read mathematics, for example formal de nitions, and to explain it in one's own words. Our observation is that students just out of high school are totally unprepared for this kind of mathematics and have a hard time learning it.
Based on the aforementioned, one could think that proofs are of no importance to software engineers. This might be true for "deep" mathematical proofs, but they de nitely should learn how to prove properties of or relations between the artifacts they produce or work with, be it speci cations, designs, implementations, protocols, or others. Such proofs are "shallow" and they have to be formal, not just rigorous, because they are mainly done by computers. No human can check millions or billions of states of a system, nor can she or he have the patience (and time!) to deductively prove some intermittent assertion produced by a proof assistant that lls several pages.
In our approach students have to do (Hoare style) correctness proofs of programs at the end of their freshmen year. Before that we teach how to do proofs in general, i.e. natural deduction style proofs in predicate logic. I personally think that one has to start that early with these topics, otherwise it is too late. I mean too late to ful ll the main purpose of teaching mathematics to software engineers: to enable them to use formal methods, i.e., methods strictly based on mathematics.
To repeat it: I think that it is absolutely necessary to teach these basic skills to enable students to use Formal Methods. But, is this also su cient? At FM conferences, especially in the industrial track, highlights of FM applications are regularly presented. Often one has the feeling that (at least) a PhD in math or CS is needed to do that work.
On the contrary, Leslie Lamport once gave a talk at a Formal Methods
Education conference with the title "All I Really Need to Know I Learned in High
School" ([
My experience shows that it takes (at least) a whole semester to teach just logic and sets, i.e., to bring students to the point where they, for example, really understand the meaning of implication, that they know that disjunction usually is used di erently in math and everyday language, that they not only are able to check the validity of De Morgan's laws by truth tables but also to use them { especially in the version with quanti ers { to express the meaning of a natural language statement in di erent but equivalent ways, and that they can work with the basic set operations (plus functions and relations, especially equivalences and orderings as required in all curriculum proposals).
Some words about where to put discrete math and calculus in a SE curriculum: I personally prefer not to have a DM course but to put most of the topics into other courses like Algorithms and Data Structures. This way you get the topics when and where you need them. If a topic is not covered there, for example modular arithmetic, then it should be taught when it is needed, say in a course on cryptography. So one can also better scale the number of proofs one does in detail. For SE students I think it is, for example, not necessary to give all the proofs concerning why RSA encryption works, computational scientists should know these proofs in detail. And if a topic does not show up in any course then it is not needed.
This does not apply to the very rst topics of DM, i.e. sets and logic. (I personally prefer to teach logic before sets, I could explain in length why.) As argued in the previous section, these basics should be put into an introductory math course for SE, and treated there extensively.
It should be clear that every engineer should have courses towards quality assurance and control that are based on probability and statistics. Here, of course, calculus comes into play. Our SE students do not have a calculus course. Calculus is reviewed during the probability and statistics course. I think this is a very good place because the relationship between summation in the discrete case and integration in the continuous case, as well as di erentiation, can be demonstrated well. Here I have to remark that this is possible in an educational system (like in my home country, Austria) where math in high school ("Gymnasium") focuses very much on calculus. If freshmen can remember anything from high school math, it is how to di erentiate and how to integrate. This may be di erent in other school systems. 4
Before I come to some "political" statements on how to enable such radical changes in the curriculum, especially towards math teaching for software engineering, I want to state that I am an educator and I belong to the people who have problems with the term "computer science" per se, and I think that the fuzziness of that term is the main reason that it is di cult to impossible to nd { and teach { the "right" mathematics that could serve the whole eld in a way that satis es everyone.
To me, the big question is the one that has been discussed for decades now, namely, the "science vs. engineering" problem. It is important to know whom we are educating: scientists or engineers? In my opinion we should not try to do both at the same time.
There is a wide spectrum of professional activities in our eld: at the one
end we have computing (computational) scientists and at the other software
engineers. It is very clear to me that the former should become full- edged
mathematicians, with an emphasis on all aspects of computing, whereby "Concrete
Mathematics" a la Knuth ([
For all that is in between { call it CS, IT, ICT, IS, IM, System Science or Engineering, Data Science or Engineering, Web Science or Engineering, Big Data, Pervasive Computing, or any other name for a (sub) eld { it is not clear to me what the right math is, and therefore I refrain from comment.
I suggest developing a software engineering curriculum incorporating mathematics as sketched above, and implementing it { more or less { independently of CS departments. Yes, and it should really be an engineering curriculum. I think that it would be good to have a "Department for Software Science and Engineering" at every institution that grants a degree in SE. This collaboration of people who are working scienti cally on foundational issues, together with others transferring their insights to engineering practices is common in classical engineering disciplines. It could help SE to become a mature engineering discipline.
My rst advice for Software Engineering as a discipline is to divorce from Computer Science. You will be the underdog in this relationship forever. Don't go in anger. Help each other, there are a lot of problems you could and should solve in common.
This is important especially for curriculum development. I see no chance that the radical changes in introductory math education I propose can be done in CS curricula in general. For new SE curricula I de nitely see the chance.
My second recommendation is to take math education for software engineers away from mathematics departments. Real (IR -) mathematicians have a hard time understanding the mathematical needs of software engineers. Many mathematicians who have an a nity towards SE and FM work in CS or SE departments anyway. Those software scientists can do the job excellently. To make it clear: math should be taught by mathematicians, but there is no need that they come from math departments.
My third suggestion is that SE should try to get integrated into the community of the old engineering disciplines as a new member. This could help SE in many, more organizational matters like accreditation, for example, to become a mature and well recognized engineering discipline. 5
In this last section I want present some personal thoughts about which advanced mathematical topics could play a major role in future SE education, as for example (partial) di erential equations do in classical engineering mathematics. The rst year of classical engineering math is usually devoted to calculus and linear algebra. Based on what I said about math education for SE, my favorite name for the course would be "Language and Methods of Mathematics".
The second year I would just call "Algebra", starting with classical topics (groups, rings, elds . . . ), enhanced by topics like, for example, process algebra, relational algebra, computational algebra. Soon I would come to a topic that I nd important for SE: algebraic speci cation of Abstract Data Types (ADT), which means students learn about heterogeneous algebras, basic notions like signatures, and also some category theory for dealing with semantics of ADT speci cations.
As computing scientists need a lot of "concrete math" a la Knuth (see [
Algebraic speci cation became popular in the early 1980s. In recent years also
coalgebraic modelling gained momentum. Finite and, more important, in nite
behavior of systems of all kinds can be modelled conveniently using a coalgebraic
approach. For a nice introduction see [
Students should learn about duality, which is one of the most important, yet basic, notions in category theory. Just "reversing the arrows" in a categorical de nition often de nes another notion that makes sense. Examples are monomorphism and epimorphism, i.e. injective and surjective functions in the category SET, product and coproduct (direct sum), initial and nal objects, pullback and pushout, and { very important { induction and coinduction for doing de nitions and proofs.
"Data processing" was an ancient name for our eld. To see that data and processes are just two sides of the same coin, i.e. dual in categorical language, the rst modelled algebraically, the second co-algebraically, is a beautiful insight that all students of SE should be able to enjoy. In this personal statement on how to make Formal Methods more popular, i.e. bring them closer to the main stream of SE education and practice, I come to the conclusion that mathematics education has to be changed in a way that students early in the curriculum learn to understand and to use Formal Methods.
In accordance with the overall objectives of the FMSEET'15 workshop, as stated in the Call for Papers, { I nd that FM education in a typical undergraduate curricula is in a sad state, almost irrelevant, { I give some recommendations for improving the situation which are mainly political and far reaching, and { I am, of course, willing to exchange knowledge and experience in any forum aiming to support FM education.