CSCI 54 "Discrete Math and Functional Programming" is the second course in our computer science sequence. Its goals are twofold: to give you a solid foundation for programming and to introduce you to formal proof.
From the course catalog:
A combined course on functional programming and formal proof. Students write programs over a variety of data structures, proving their programs correct with respect to precise logical specifications. Programming topics (and proof topics) range over: recursion (induction); combinatorics; algebraic data types, from lists to trees to abstract syntax trees (structural induction); parsers and interpreters (soundness properties); regular expressions (set theory and language theory).
Prerequisites: CSCI051 PO or equivalent (e.g., 4 or 5 on AP CS exam). You may not take this course if you've already started the Harvey Mudd introductory sequence.
This course is taught by Joseph C. Osborn. The TAs (in alphabetical order) are Joram Amador (our BBICS mentor), Summer Hasama, Liz Johnson, Ethan Lee, Maika Nishiguchi, Sophia Ristuben, and Rachel Yang. Contact them on Zulip only, not Slack or email!
We'll be using Zulip for this course; you can get connected with this link.
Contact Prof. Osborn if you are having trouble logging on or joining the channel.
We’ll be using Coq 8.14.1, though any version 8.9.1 or later should work. Install the "Coq Platform" appropriate to your computer.
We recommend Emacs or Overleaf for editing LaTeX later in the course.
Hi there! Let's take a little break from the formal syllabus language.
54 has a bit of a reputation for being very difficult, with too much homework and too many ideas crammed into one semester. This is partially because it used to be two courses (we joined them together with an "and"). Since 2018, Prof. Greenberg and I have worked to refine the course---while nearly every student passed every semester, it put a lot of undue stress on students; we have gradually improved the pacing and delivery over time as we learn what works and what doesn't.
In particular, this class will feel somewhat shocking if you are used to being "good at" programming (whether that means you aced 51 or skipped 51)---it requires "muscles" that you are not likely to have developed, and you may have the experience of being a novice again and not knowing where to even start on problems. Please try not to be discouraged if this happens: it means you are learning something brand new! If you are feeling this way, it is nearly certain that your peers are too (and candidly, your instructor also had this experience when learning this material for the first time).
I promise to work with you if 54 isn't working for you, if you promise to let me know when the pieces aren't fitting together.
The course home page has a listing of the planned material. Lectures are posted as pre-recorded videos on Box. Class is activities plus Q&A, with minimal talking.
This class is challenging and sometimes students feel isolated in their difficulty. To combat this, in-class activities and out-of-class mentor sessions will take place in learning communities, a persistent group of students with whom you will meet weekly. LC participation is mandatory, though the mandatory part can either be achieved during class or outside of class. Each LC will be assigned to one TA.
Moreover, each week you'll have a homework buddy in your LC. You and your buddy are responsible for checking in with each other once per week.
Prof. Osborn will hold office hours for a half hour after class on Tuesdays and Thursdays, 9:30--11:00 AM on Wednesdays, and other times by appointment (see the course website for scheduling information and mentor sessions).
Two thirds of the course will use Coq as the main grader: if Coq accepts your proof, it’s correct! The remaining third of the course will be on paper proofs, which will be graded by hand. There will be in-class quizzes, but they will not be for credit.
In order to obtain a grade for a homework, you must both turn it in on Gradescope and check in with a TA or Prof. Osborn for credit. This is an opportunity to walk through the non-automatically-graded aspects of your homework like style, new definitions, or informal proofs. It can also be an opportunity to earn credit back for minor errors or misunderstandings. It is not an opportunity to have one-on-one, impromptu office hours.
Your grade for the course will be determined by your aggregate grades on:
Each homework and exam will have a variable number of points. Homework grades are based solely on check-ins, so the 25 homework grade points are the proportion of homeworks which were successfully checked in. Exams are graded by section and all sections are weighted equally.
Each class day corresponds to a short homework. Homework is due at 11pm PT on Monday nights; submission is on gradescope.
Homework will be a mix of Coq programs, Coq proofs, and paper
proofs. Coq code will be turned in as a .v file; paper proofs will
be turned in as PDFs rendered by LaTeX.
Homework that doesn’t compile, due to syntax or type errors, gets no points.
Pair homework submissions are allowed, but you may not pair with the same person twice in a row. Be sure to tell Gradescope that you are submitting pair work. I emphatically do not recommend a "divide and conquer" approach to pairing, as then each student will have only half an understanding of the homework; instead, work on the same part of the homework at the same time, together.
This course is rife with dependencies and is very homework-oriented; almost all of the learning you do will happen while you’re doing homework! (We think the lectures are good too, but let's not get ahead of ourselves.)
Accordingly, late work will not contribute to your grade. We will, however, review it with you.
Exams work a little differently in this class. I believe that exams should be an opportunity for learning, not a punishment for studying the wrong things.
First, this means that each exam is take-home, open book and open notes---the same rules as homeworks, except that you may not collaborate with other students on exams.
Second, I'll provide a study guide (a list of ability questions which can help you come up with practice questions and decide whether you know the material) broken down into sections for each exam. No question will be on the exam that covers topics included in the study guide.
Third, I will provide example questions so you will be familiar with the format of exam questions---no surprises there, either.
Finally, students may opt to improve their grade on any question from any exam by an in-person oral exam on the question, which might include the student explaining the problem with their original answer or solving an alternative question.
Learning any new language is challenging, and Coq is very different from conventional programming languages. We encourage you to help each other learn the language and we also encourage you to discuss the text.
However: all work in the course must be your own. As explained in the student handbook, this means that the work you turn in must represent only your own work. It must not be based on help from others or information obtained from sources other than those approved by the instructor. Examples of acceptable sources of information include:
Examples of unacceptable sources of information include Stack Overflow, Quora, and your classmates’ code.
You should never read or copy another student’s solutions (code or otherwise), exchange files, or share your solutions with anyone else in the class until after everyone involved has turned in their work. If a discussion with another student helped you find your answer, mention that in a comment. It’s hard to tell the difference between uncredited help and plagiarism (because they’re the same thing).
If any of this is unclear, please: just ask.
Failure to abide by these rules is considered plagiarism, and will result in severe penalties. The first offense typically results in failing the assignment and referral to the appropriate college office or committee—which may mean further consequences. See the CS Academic Honesty Policy and Pomona Academic Standards for further information. Please don’t put anyone—me, you, or anyone else—in this unpleasant situation.
Pomona students seeking academic accommodations should contact disability support at the Dean of Students Office. You’ll need to meet with them to discuss appropriate accommodations and provide documentation as necessary.
Students from other colleges should contact their home college’s disability coordinator for accommodations. The coordinators are, to the best of our knowledge:
The Quantitative Skills Center (QSC) provides academic support to Pomona College students in courses that feature a large degree of quantitative and/or scientific reasoning through our QSC Partners Program. QSC Partners meet one-on-one with students to provide support for a variety of Pomona courses for course specific help. The QSC also offers non-course specific help in general quantitative skills and offers consultations for projects and theses involving quantitative methods. Additionally, Dr. Travis Brown, Director of the QSC, and Dr. Dylan Worcester, Assistant Director of the QSC are available to meet with you regarding your success in STEM at Pomona College. To make an appointment at the QSC, please log on to the Portal and go to Academics > Quantitative Skills Center, or contact us at qsc@pomona.edu.
The faculty at Pomona College knows that person-to-person interaction provides the best liberal arts education. The best learning occurs in small communities. This year we are gathering in person for what we do best: create, generate, and share knowledge. During the past academic year, we built community remotely, and this year we will build on the pedagogical improvements we acquired last year.
Our health, both mental and physical, is paramount. We must consider the health of others inside and outside the classroom. All Claremont Colleges students have signed agreements regulating on-campus behavior during the pandemic; in the classroom, we will uphold these agreements. We need to take care of each other for this course to be successful. I ask you therefore to adhere to the following principles:
The pandemic is fast-moving, and we might have to adjust these principles as the semester evolves. I am always happy to receive your feedback to make this course work.
Let’s care for each other, show empathy, and be supportive. While there will likely be some community transmission and breakthrough infections, together, we can minimize their effect on our community and on your learning.