Story | Olivier Danvy (he/him)

Editing | Cindy (she/her), Managing Editor; Soroush (she/her), Copyeditor

Photo | Joshua Vargas (he/him)

”Introduction to Computer Science” (YSC1212, Intro to CS for short) and ”Proof” (YSC2209) did what they could to patch the blind spot in the college’s common curriculum – namely no Computer Science and no Mathematics [2]. And so in the second week of Intro to CS, the students are made aware that there are many notions of computations, and that for each of them, there are many notations (a.k.a. programming languages). Like natural languages, programming languages are specified with formal grammars. However, where the grammar for a natural language is descriptive at best, it is prescriptive for a programming language, hence the notoriously incontrovertible syntax errors in one’s programs: The computer doesn’t ”see what we mean,” not just because it doesn’t see, but also because most of the time, what we mean is a work in progress. The students are also made to realize that in programming languages, formal grammars can be used to generate syntactically correct, but semantically random sentences. By the fourth week, they are introduced to random-number generators, so they can program their own generators of grammatically correct sentences. Thus, in the spring of 2021, just in time for Valentine’s day, Leonard Tng programmed the generator of love letters at https://lovelettergenerator.com. (Rumour has it that some of these letters were facetiously field-tested on Tinder and that somehow, they did not fare well at all.)

Good times.

In “Functional Programming and Proving” (YSC3236, FPP for short), the students are made to realize that mathematics and statistics are expressed in a language that can also be formalized with a grammar, and that logical statements and their proofs can be checked. Therefore, proofs are not a subjectively convincing argument, nor a mere social convention: They have a concrete, quantified existence that is rooted in linguistics and mathematical logic and that can be checked independently and objectively. In FPP, we use The Coq Proof Assistant to write programs and proofs, based on the correspondence between propositions and types. That semester, our students write more proofs as well as longer proofs than they had ever done before in their life. FPP, like Intro to CS, is very much hands on, so by the middle of the semester, the students are asked to formalize and to prove that the product of two consecutive natural numbers is even, a deceivingly simple exercise that makes them mobilize everything basic they know about programming and proving in a safe setting and in a way that scales beautifully.

Good times too.

Here is how ChatGPT fared with that simple exercise on Monday 6 February 2023, a candid reminder of Ted Chiang’s Lifecycle of Software Objects [1], to say nothing of Ken Liu’s Perfect Match [3]:

Q. Is the product of two consecutive natural numbers even?

A. Yes, the product of two consecutive natural numbers is always even.

Q. Why?

A. Because if you have two consecutive natural numbers, one of them must be even (for example, if you have the numbers n and n+1, then n must be even). When you multiply an even number with any other natural number, the product will always be even.

Q. Is the product of three consecutive natural numbers divisible by three?

A. Yes, the product of three consecutive natural numbers is divisible by 3. Since consecutive natural numbers differ by 1, the three numbers must have a sum of 3 times the middle number, which is divisible by 3. The product of any multiple of 3 with any other number is also a multiple of 3, so the product of the three consecutive natural numbers is also divisible by 3.

Q. Is the product of four consecutive natural numbers divisible by four?

A. No, the product of four consecutive natural numbers is not necessarily divisible by 4. While the product of the first two consecutive natural numbers will always be even, it may not be divisible by 4. Whether the product of four consecutive numbers is divisible by 4 depends on the specific numbers involved and cannot be determined just by the fact that they are consecutive natural numbers.

The answer to the first question is correct, but its argument is incomplete (the claim should be “if you have the numbers n and n+1, then either n or n+1 must be even”).

The answer to the second question is correct, but its argument is off (involving a sum?).

The answer to the third question is incorrect. (The two first numbers are consecutive and therefore their product is even, and likewise for the two last numbers. And multiplying two even numbers (say, 2x and 2y) yields a number that is divisible by four (namely 4xy).)

**References**

[1] Ted Chiang. *The Lifecycle of Software Objects*. Subterranean Press, 2010.

[2] Pericles Lewis. In Asia, for the world: The creation of Yale-NUS College. Symposium on Globalising the Liberal Arts, June 2016. https://campuspress.yale.edu/pericleslewis/ in-asia-for-the-world-the-creation-of-yale-nus-college/.

[3] Ken Liu. *A perfect match*. Lightspeed Magazine, December 2012

[4] Dean Martin and Foster Brooks. The Bar. https://www.youtube.com/watch?v=F662rWlkzrI.

Addendum (revised on 12 Mar 2023):

The title of this article is a quote from The Bar, and is meant to illustrate the contrast between a blind watchmaker, a drunk inference maker, and an idiot not very savant.

Olivier Danvy is Professor of Science (Computer Science) at Yale-NUS College. He is pretty good at `l’esprit de l’escalier <https://en.wikipedia.org/wiki/L%27esprit_de_l%27escalier>` and can be contacted at danvy@yale-nus.edu.sg.

*The views expressed here are the author’s own. The Octant welcomes all voices in the community. Email submissions to: yncoctant@gmail.com*.