Why do universities not teach constructive mathematics to CS undergraduates?

Question

I had a conversation with a user on the Internet. And it did indeed wake my interest regarding something that I had also been asking myself long ago. Why do so many universities still teach beginners in computer science classical mathematics and not constructive mathematics which seems a lot more useful in the field of computer science? I always wondered about that and thought that maybe there would be reforms that take a different philosophical approach into constructivism.

To quote a few statements from the user I discussed with here:

Why do you think you're so great for knowing that constructive math exists and not being careful enough not to send novices on a four-year journey into debt to study math they don't need, while your colleagues in academia misunderstand exactly what math is required for computer science academics?

Why do you allow your peers to waste my future employees' time teaching them Calculus I, II, III?

The user seems to come from a non-academic field (I believe?). But does he have a point? Or is it just ideological rambling? Is teaching classical maths really just a waste of time to CS beginners? If that is the case, why hasn't been there any change regarding this?

Answer 1

Let me offer a few thoughts, specific to mathematical pedagogy in computer science (in particular for the states):

(a): a typical BS computer science program barely has time to touch on computational theory, further still computational theory in which the difference between classic and constructive mathematics matters. For reference, here is a sampling of the typical undergrad CS major within the first three years, easily verified via looking at syllabi:

Math: calculus, linear algebra, ODEs, physics, graph theory/combinatorics, probability, optimization, numerical analysis in addition to computer science-specific courses, in particular data structures/algorithms/assembly/web design/OS/theory.

That leaves approximately one year- in addition to general education requirements- for extra math courses.

(b): the CS major thus has a choice between extra math courses and courses to boost their skillset/resume. Since a majority of students will not go into academia, it is clear that it is better to take CS electives, such as NLP, AI, etc. Why reshape mathematics pedagogy for these students?

(c): even for those who do, their current math education is approximately equivalent to a second-year maths student. The next jump, with respect to theory, is grad first-year theory A and theory B (roughly algorithms and logic/semantics). Issues of constructive logic will mostly affect theory B (in practice, if not in principle). This brings us to our next point...

(d): the difference in constructive, vs classical logic, will roughly come down to choice, LEM, or double negation (in fact these are equivalent given that the rest of the system is typical). But if one is mathematically advanced enough to be doing work in theory B, this is generally a small modification- simply do not allow proofs via these methods. So in fact, especially for computer science (it's another story, for, say real analysis), the difference tends to be small.

*unless one is actually proving things about certain logic. But this is in general beyond the scope of a first-year grad course. And if one is advanced enough to be doing this, then they are typically fluent in moving between classical and constructive paradigms, anyway.

(e): but most mathematics is done in classical logic. Since the math courses will in general be taught by the math dep't, many who will assume LEM/choice/double negation, they have the choice of altering pedagogy for a very small population, for which the difference is negligible, or continuing to prep the large majority of students for how math is "typically" done. If one accepts classical mathematics, it is easy in principle to make students aware of the general issues of classic vs constructive mathematics. But one would never limit themselves, just like a programmer would be unlikely to only use functional paradigms if they "believed" in object-oriented paradigms/states. Similarly, one is unlikely to not use double negation, choice, etc. if one sees nothing wrong with it.

Answer 2

"Constructive mathematics is distinguished from its traditional counterpart, classical mathematics, by the strict interpretation of the phrase “there exists” as “we can construct”."

The viewpoint of constructive mathematics is not generally accepted as a basis of mathematics. It is the viewpoint of a minority - of course, I do not mean this as a ranking about the scientific value of both approaches.

Computer science relies on mathematics as a supporting discipline. The subject of computer science are not sophisticated discussions whether indirect proofs are admissible or not. It is much more important that students of computer science learn how the formalization of a statement or a theory looks like and what a correct proof is. And that they acquire some experience by doing exercises by themselves.

Hence I consider it justified to teach students of computer science and also undergraduates of mathematics the usual courses: Calculus, linear algebra, graph theory and some basics from mathematical logic and set theory.

Answer 3

So we're clear, mathematical constructivism is a logic/philosophic approach to conceiving mathematical activity. That's pretty remote from undergraduate CS pedagogy. From WP:

In the philosophy of mathematics, constructivism asserts that it is necessary to find (or "construct") a specific example of a mathematical object in order to prove that an example exists. Contrastingly, in classical mathematics, one can prove the existence of a mathematical object without "finding" that object explicitly, by assuming its non-existence and then deriving a contradiction from that assumption. Such a proof by contradiction might be called non-constructive, and a constructivist might reject it. The constructive viewpoint involves a verificational interpretation of the existential quantifier, which is at odds with its classical interpretation.

When I got my undergraduate degree in CS almost 25 years ago, it was a whiz-bang tour of the basics. In fact, we had a lot of students who had almost some to none experience with a compiler in our program. Computer science is a big topic. For other readers, it might help to review those ideas here on with this introduction to computer science. (YouTube). In the days of Mauchly and Eckert, the lead inventors of ENIAC, computer scientists were mathematicians. Computer science as a distinct discipline grew into it's own long ago. In fact, some of the concerns from eminent computer scientists, such as Leslie Lamport (of LaTeX fame), is that there's not enough mathematics in computer science currently (Quanta). The reason for that is simple, CS encompases a host of topics like cryptography, computer engineering, operating system design, algorithms, programming languages, computability and complexity theory, grammar and automata, software engineering, and AI just to begin with. Most CS undergraduates get in some calc (maybe up to diff EQ) and stat, and then some discrete math relevant to the major. The notion that a CS undergraduate would engage in the formalisms of intuitionism is far-fetched, because the nuances of formal systems of logic aren't covered in depth.

In fact, covering the philosophies of mathematics, computer science, and AI, I suspect might be required at most as a single course, though nothing like these philosophical topics were covered in my coursework in either of my mathematics or CS undergraduate degrees or even in my masters. Whoever was the source of your quotation, I would say that they have some strong feelings about philosophical positions that leak out into an editorial that has little insight into the education process, at least here in the US. Perhaps Germany, Norway, or the UK it's a different story. I would definitely use a single phrase regarding the succinct editorial presented above: cum grano salum.

Answer 4

So there's something which might be worth discussing here; namely, given that the primary dispute between constructivists and classical mathematicians relates to the transfinite, does the dispute matter at all to the undergraduate Computer scientist who works in the realm of the finite?

Well, if we're taking the conversation to metatheory, then yes, of course it matters. But methodologically, does metatheory matter at the undergraduate level? If we aren't interested in pushing forwards the boundaries of the field yet, but simply at helping people understand the existing well-worn terrain, then what space is there in an undergraduate computer science curriculum to devote to this issue?

Undergraduates have other methodological skills needs that we really need to be starting with - information literacy and critical thinking, research and study skills, time management, communications and team working, project management, self-care and motivation and so on. If they're able to gain these and grasp the fundamentals of the course, then a postgraduate level is a good time to talk in depth about philosophy.

If there were more at stake in the actual results of the field then a philosophical discussion might have needed to happen earlier, but since constructivists and classical mathematicians agree with respect to the finite, that's a conversation that can wait until the student has developed as a scholar.

Answer 5

Due to many reasons, main ones are follows:

1. It is computer science program, and not philosophy program. Certainly, foundations are in philosophy (mathematical logic), but curriculum focusses on well-established topics (immune to philosophical objections).

2. Expectations from the program are to produce engineers and technical researchers, not philosophers.

3. Undergraduate curriculum is fully packed. Literally, it is packed with assignments, lectures, tutorials, labs. You don't want to bother undergraduates with philosophical problems -it defeats the purpose of the program. There is too much already.

4. Philosophical points of view are not completely ignored. They are mentioned, in passing, in selected courses -theory of computation, logic, etc. A genuinely interested candidate will eventually investigate theorems of Godel & Turing. In that sense, it is best to let students who are able to see philosophical problems approach on their own. Why impose things which don't make sense universally -it is philosophy after all, and this is not a philosophy program.

Answer 6

There seems to be three questions here:

• Why not teach nuanced philosophy
• Why not teach constructivism, a particular approach to mathematics
• Why are you even teaching Calculus I

Why teach Calculus is probably an oddball that I wont answer here, but I think I can point to the reasons for the first two as a single answer by pointing out what we don't teach: the actual physics of computers.

Computer science's products are 100% part of the physical computers we run them on. We inherit all of the physical limitations therein. That being said, we still teach students to think about computers as Turing machines, despite the fact that I have never once in my life been shown a computer with an infinitely long tape. To be technically precise, we should be teaching computers as finite automata (and then perhaps delve into the electromagnetic realities of the chips).

I think this disagreement between theory and practice is far greater than the distinction between different shades of theory. I don't think an undergraduate benefits from such philosophical distinctions when operating on the wrong structures. That being said, the model of a computer as a Turing machine has had enormous practical success. I like to think that practicality has something to do with undergraduate degrees.

As a practical example, consider the Coppersmith-Winegrad algorithm. It is a matrix multiplication algorithm with a complexity class of O(n^2.3728642...), making it asymptotically the fastest matrix multiplication algorithm in existence (after several upgrades by other authors). An undergraduate might know of it. Why? It may have been given as a counterexample for why complexity classes should not be treated as the end-all measure of efficiency. The constants associated with the algorithm are so great that it is not known to beat the next fastest algorithm, based on the work of Strassen, for matrices which are small enough to fit in a supercomputer's memory.

With arguably "fuzzy" things to learn such as the limits of using complexity classes, how would one rank learning the limits of different approaches to mathematics?

Answer 7

Interesting question. I suspect there could be researchers who thinks similar to this person (well, except for the Calculus dismissal). The following is about how people writes software today and how constructive math/logic could be relevant in a very practical sense in the future for that task, it is not about the philosophical position.

I think this person might have a point if he is ready to defend an hypotetical future where:

1. Software development is solely grounded by the so-called Formal Methods, i.e. that the development of software should be guided by logic and math in order to guarantee correctness. Some people think this is the most ''true engineering'' you could get instead of the otherwise more ad-hoc ''just code then run some tests'' method which surely represents about 99% of software industry today. The other 1% is represented by the more niche ''critical systems'' (software in trains, planes, medical devices, etc.) for which lives matter and there is a bit more of rigor involved along some actual ISO standard to fulfill (but still, not even this 1% relies only on Formal Methods, in fact there is no current ISO mandating Formal Methods although they are certainly recomended).
2. But wait... lot of Formal Methods (in fact, the most popular ones i believe, e.g. Z, B, TLA+, Dafny) are based on classical logical frameworks like ZFC and the like. After all, set theory is still popular, even with type theory and category theory around the corner gaining much attention recently. So another condition we requiere in this hypotetical future is the accepted supremacy of the constructive Formal Method approach which is intimately tied to typed functional programing languages through the Curry-Howard correspondence. Apparently, in this future programmers will only program in very very strongly typed functional programing languages (akin to Agda, Coq, etc.) where the type checker can verify that the code have the type-asserted properties, honoring the old slogan "if it compiles, it works". So, no run-time surprises. (even something like Rust does not come close to this, but is a step forward in this direction, and is getting attention).

If this hypothetical future materializes, i think the relevance of the constructive point of view would be unquestionable and you get close to discard classical logic. Because in this case it is not just a matter of "philosophical position" as others have asserted (i obviously understand the other answers are trying to be realistic).

Now, for a dosis of reality:

1. It is hard to believe in a future where the main goal of software is to be ''correct'' in the strong logical sense of the word. Software development is not a regulated activity like other engineering branches, and there will always be room for sloppy software. Of course, the need for rigorous methods surely will grow, but how much?. One could dream a future where programmers at least use "certified" compilers like the CompCert, but that is not enough to make classical logic obsolete.
2. So, will programmers finally liberate from the Von Newman style?. This was Backus question decades ago. It seems a lot of research went to create very high level languages, declarative instead of imperative, to favor mathematical reasoning abstracting programmers away of hardware. But hardware is imperative, it is about state and how you change state, this is the physics land where we are still discovering new physical limitations that challenge the way hardware is designed. There will always be room for a low level world where people uses low level languages and tools which can still benefit from ordinary math and logic, the same math any branch of engineering uses (imagine asking an electrical engineer what "kind of math" he uses or if he uses LEM regularly, he surely will tell you that math is math and what the hell are you asking). For this kind of people, programs are not just logic, they care about the physical execution of the programs. I don't see this people buying the "a program is a proof" argument, because they have no use for it. They know, because hardware is physical, that computation can't be really proved "correct", you need to go empirical and accept sufficiently small probabilities of failure. For me, this will ever be at odds with the high level view where software is treated as a purely logical artifact (because, what are the laws of software if not some logic?), the modus ponens land, where there is much people searching (or inventing?) the best logical foundation and debate about if it is valid or not to use LEM in this foundation.
3. Why we should prefer the constructive Formal Methods (type theory based) over the non-constructive Formal Methods (mainly set based)?. One of the differences, and the most important, is that constructive Formal Methods aims to formally verify actual software code (or something from which you can extract executable code), while the others typically aims to formally verify design models of the software leaving a gap between the design and the implementation (code extraction is in principle possible but not typically the goal). We should recognize the former is much more ambitious, however the latter results in a usually more flexible and light weight method of verification more amenable to typical industrial use. It is not clear to me if the relative benefit of doing the former outweighs a combination of current standard practices like normal testing plus the use of non-constructive formal methods applied at design phase (in fact, companies like Amazon had success using formal methods for the design of distributed systems, and this is not what is usually considered a "critical system"... but guess what, money is also critical!). Sure, you could think that we can also use constructive Formal Methods just for the design and not necessarily for the implementation, but then there is no need to be constructive here unless you are a constructivist by hearth and then you are just making your choice.

Finally, i don't know exactly what is his problem with Calculus, but in line with previous considerations, i guess this is an individual obsessed with software correctness who ignores or does not care about the more quantitative performance aspect (e.g. time resources) which is closer to physics and typically evaluated using ordinary mathematics rather than formal logic (i mean... he clearly is not the Knuth type, and surely can't be working with modern AI either).