The events leading to the term project and the oral exams

Every week (except before recess week and at the end of the semester), there will be mandatory exercises, to be solved in groups of 8(ish) and uploaded on Canvas.

The rationale for 8 is that the lecturer will then have 6 handins to correct per week, which is doable with high-quality feedback. In turn, the handins are expected to be of high quality.

Expectations

• Each weekly handin is in 2 parts:
  • the exercises proper (as a .v file), solved in group, and
  • a joint report (as a .pdf file), spell checked.
• The midterm project is in 3 parts:
  • the project proper (as a .v file), carried out in group,
  • a joint report (as a .pdf file), spell checked, and
  • an individual oral exam.
• The term project is in 3 parts:
  • the project proper (as a .v file), carried out in group,
  • a joint report (as a .pdf file), spell checked, and
  • an individual oral exam.
• The goal of the oral exams is not to trip you. Each one should give rise to a pleasant 20-minutes conversation where you demonstrate that you can start Emacs, compose a .v file with a simple program, a simple property of this program, and a simple proof of this property; and that you can explain what you are doing. This program and property will typically be ones that we have studied in the course of the semester – most likely a variation on one of the project tasks.
• The grade is based on the following percentages:
  • 10% for participation and non-mandatory exercises (in the weekly handins and in the term project),
  • 30% for the weekly handins,
  • 15% for the midterm project, and
  • 15% for the term project, and
  • 30% (12% + 18%) for the individual oral exam.

Template for the reports

Here is a LaTeX template for the reports and a listing package for tCPA, lstcoq.sty. This particular template assumes a .v file “file1.v” that is is in the same directory.

On generative AI

In this course, the attendees are made to realize that mathematics is expressed in a language which can also be formalized with a grammar, and that logical statements and their proofs can be checked. So proofs are neither a subjectively convincing argument and even less 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. Using the Coq Proof Assistant, which is based on the correspondence between propositions and types and between programs and proofs, the attendees are to write more proofs as well as bigger proofs than they had ever done in their life so far.

This course is very much hands on, and so by the middle of the semester, the attendees 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, a testament to sound foundations.

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:

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

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

17. Why?

1. 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.

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

1. 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.

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

1. 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)).

Caveat emptor.

Postlude

Halcyon: What is the point of the little romp with ChatGPT just above?

Na-bong: I think it is a cautionary tale.

Halcyon: So we shouldn’t use a generative AI to solve our exercises and to write our reports?

Na-bong: Well, you exercise physically, right?

Halcyon: Yes, and, huh, thanks for noticing.

Na-bong: What do you do?

Halcyon: Jogging.

Na-bong: That’s inefficient. Why don’t you take the bus instead?

Halcyon: Well, that’s not the point. Oh. You mean that we exercise intellectually by solving our exercises and by writing our reports?

Na-bong: Yup. Which is the better gift for your grandmother: a program that solves Sudoku puzzles or a program that generates them so that she can solve them herself?

Halcyon: Regardless, in this evolving 21st century, we also need to learn to ask the right questions.

Dana: And to ask questions, we need to know something about things.

Halcyon: Right. If one can ask questions, one is already half there. The problem is learners who don’t understand enough to ask questions.

Alfrothul: We also need to be able to gauge answers, like in the little romp above.

Mimer: And all of that is the point of your education.

Halcyon: So, no use of a generative AI in this course?

Mimer: No use of a generative AI in this course.

Version

Added lstcoq.sty, thanks to Wong Kok Rui’s eagle eye [24 Jan 2024]

Added the section about generative AI and the postlude [19 Jan 2024]

Created [18 Jan 2024]