General Information
How can I get help in 6.S057? Who should I ask?
For help on assignments, visit office hours for the most effective help.
For most questions, post on Piazza.
Do not post code on Piazza. If you are tempted to attach code to get help with fixing it, please come to office hours and get help in-person instead.
You cannot submit problem sets on Piazza or by email; you must submit them on Gradescope.
If you have a problem with a grade, see: what do I do if I have a question about grades?
If your problem is confidential or involves S3, email
6.S057-personal@mit.edu.
Please don’t email individual instructors or TAs or post on Piazza only to specific staff: use 6.S057-personal for confidential issues or post on Piazza without picking specific recipients. This convention will help us make sure the right person sees your question.
What is 6.S057?
This experimental offering attacks some of the core material of 6.102 (Software Construction) from a different perspective. The core question of both classes is “how do we build and maintain large software systems in a way that helps us meet high standards of quality?”. This class takes an approach more heavily grounded in logic and mathematics, where we will actually spell out what “quality” means for different programs and use software tools to guarantee mathematically that the code we wrote achieves our objectives.
What does “experimental” mean?
It means 6.S057 is a new course, using new materials, assignments, tools, and policies that are still under development. We are very interested in your feedback to help the course improve, and we also need to ask for your patience if and when there are problems or we need to make unexpected changes!
Objectives
In the language of formal logic, explain what it means for a program or its parts to be correct. (These explanations are called specifications.)
Write code sprinkled with annotations related to explaining why it is correct, such that an automated correctness checker is satisfied. (This activity is called program verification.)
Plan the structure of a program for simplicity of understanding it in parts, which helps both program verification and readability by humans. This activity includes designing parts to have simple, self-contained specifications. (This aspect is perhaps the intellectual core of the whole subject, relating to the ideas of abstraction and modularity that are emphasized even in more-conventional classes on software engineering.)
Develop code in the particular verification-enabled programming language Dafny, though the key takeaways apply more broadly.
This class is designed to be useful even for students who never do formal program verification again! The mental habits we’ll build should pay off in designing maintainable software systems with clean interfaces between components.
Differences from 6.102
This class is distinguished in covering the theory and practice of program verification, as sketched above and elaborated in the first classes. 6.102 involves only informal reasoning about functional requirements and correctness of code.
What do we not cover from 6.102, to make room for program verification? We don’t cover how to build software in teams (there is no group project), and we don’t practice code reviewing or using version control. We also use a different programming language (Dafny vs. TypeScript), leaving students with different practical skills in particular languages, though the big ideas of program structuring are the same. We skip covering systematic testing, a key topic from 6.102, because program verification is more comprehensive (if much less commonly used in industry today). And we do not discuss concurrency, another major topic from 6.102.
This semester’s offering is available to petition the EECS Department as a substitute for 6.102 from the perspective of degree requirements. Follow-on classes may, however, not consider 6.S057 as an adequate substitute from a prerequisite perspective, for instance if they want to make sure students have experience in team software-engineering projects.
Classes, readings, and nanoquizzes
Class meetings. There are two 90-minute class meetings each week on Monday and Wednesday. You are expected to attend class and to participate actively in exercises. The course calendar shows all the dates of the class meetings.
Laptops required. Classes will include nanoquizzes and programming exercises that will require a laptop set up with the course tools. If you don’t have your own laptop and you need to borrow one, IS&T has a short-term laptop loaner program that will lend you one. Alternatively, EECS has a loaner program (with very limited computers) that can be extended throughout a semester. Email Dr. Amanda Beyer-Purvis for more information.
Course readings. Each week will have a reading that you must read, with online exercises to complete. In general, each reading is an introduction to a pair of classes: the first reading is an intro for classes 1 & 2, the second reading is for classes 3 & 4, and so on. A reading with its exercises is due the night before the first corresponding class (except for the very first reading). Deadlines are shown on the course calendar. The online exercises are part of the classwork grade described below, graded based on completion, not correctness.
Recommended reading: Program Proofs by Rustan Leino. For a book-format introduction to Dafny and treatment of the ideas in this course, this book is the recommended resource. Each course reading mentions the relevant chapter(s) in Program Proofs where you can turn for more details or just a different presentation that may use different examples.
Nanoquizzes. Frequently a class meeting will include a short quiz on: the course reading for that class, recent previous readings, and/or recent previous classes. Nanoquizzes are closed-book and closed-notes, with a short time limit. Some nanoquizzes will be on paper, to provide practice working problems on paper as you will during the exams. Other nanoquizzes will be on your laptop. The nanoquizzes are part of the classwork grade described below, graded for correctness.
In-class exercises. Most class meetings will include programming exercises done in pairs. You will need to collaborate using Constellation to receive credit for these exercises. If you encounter technical issues, please take note of the automatic-makeups policy below, and please visit office hours to resolve the issue for next time. You are not expected to complete unfinished exercises after class, but staff will be happy to help you review or finish them. The exercises are part of the classwork grade described below, graded based on effort, not correctness.
Limited laptop use. Your laptop is a necessary tool for in-class exercises, but it also presents a huge opportunity for distraction. The price of that distraction is paid not only by you but by all those around you who can see your screen. For that reason, we will ask you to fold down your laptop screen when we are not working on an exercise.
If you want to take notes using a device, that device must lie flat on the desk so that the screen is not propped up and visible to others.
Classwork grading. Each course reading (graded as the fraction of exercises completed), each nanoquiz (graded as a quiz), and each class with pair-programming exercises (graded for making progress on the problems, weighted average) contributes a grade to your overall classwork grade. The classwork grade is computed as the average of all these individual grades, after applying the automatic-makeups policy below. A class with none of those components does not contribute to the classwork grade.
(Reading-exercise completion is shown on Canvas. Nanoquiz and in-class-exercise grades will be published to Canvas after grading.)
Automatic makeups. The lower bound for each component of your classwork grade is your grade on the next exam covering that material. Classes 1–15 are covered by Exam 1, and classes 16–25 are covered by Exam 2. If you forget to do a reading, miss a nanoquiz, or can’t complete some exercises, that grade is replaced by the corresponding exam score.
This means that if you are absent or if a technical issue prevents you from participating, you will automatically make up any missed or low classwork grade when you take the corresponding exam. You do not have to tell us which grades you want to make up this way; it happens automatically.
No other makeups. The automatic makeups apply to all reasons for missing class or getting a low classwork grade.
Problem sets and automatic slack days
Problem sets. You will complete weekly problem sets. These are individual assignments, and you can read the collaboration and AI-tools policy for problem sets.
Grading will be mostly automatic, based on which parts of a program you convinced Dafny are correct!
Late problem sets. You may submit a problem set up to 1 day late (24 hours) for 75% credit and up to 2 days late (48 hours) for 50% credit.
Automatic slack days. At the end of the semester, we will automatically remove the 10 days worth of lateness penalties that most benefit each student.
This built-in flexibility is intended to help you manage periods of heavy workload, minor illness, absence from campus, and other unusual circumstances.
Slack days are atomic; you can’t chop them up into slack hours or minutes. If you unable to submit an assignment on time, go to bed and sleep and ask for help or keep working with fresh eyes in the morning.
If you are experiencing serious personal or medical difficulties that prevent you from completing work on-time, please talk with a dean at Student Support Services. With their support, we can consider additional extensions, but your circumstances will have to be extreme to justify the special request.
Exams
Exams. There will be two exams. Exam 1 is shown on the course calendar, and Exam 2 will be held during the final-exam period, so its date and time will be announced on the final-exam schedule.
Each exam will be comprehensive, drawing on any topics covered up to that point in the course, so e.g. Exam 2 may include topics that were already covered on Exam 1.
Exam 1 will be 50 minutes long, and Exam 2 will be 75 minutes long.
On paper. The exams will be given on paper.
Some of the in-class nanoquizzes will also be done on paper, as practice for answering the kind of questions that may appear on an exam and as practice for working with only pencil and paper.
Closed book. You may not use notes during the exam, and you may not use electronics of any kind.
Practice materials. This is an experimental offering, so we do not have an archive of past exams you can use for practice, but we are designing the nanoquizzes to provide the right kind of practice.
Academic integrity
This topic has its own page on Academic Integrity: collaboration, AI tools, and public sharing.
Grading
The relative contributions of the various elements to your grade are:
- Problem sets: 40%. Each problem set will have approximately equal weight, but we may make small adjustments based on length or difficulty.
- Exams: 50%. Exam 1 is worth 20%, and Exam 2 is worth 30%.
- Classwork: 10%. Determined by grades on nanoquizzes, completion of reading exercises, and effort on in-class exercises.
Letter grades. Overall letter grades are determined at the end of the semester. The default cutoffs are: a final average of 90 and above is an A, 80 and above is a B, 70 and above is a C. These boundaries may be adjusted downwards if necessary because of the difficulty of the assignments or exams, but the boundaries will never be adjusted upwards, so a final average of 90 is guaranteed to be an A. The boundary adjustment is done heuristically, and there are no grade quotas, no grade targets, and no centering of the class on a particular grade boundary.
Individual consideration. Every student is considered individually in the final grading meeting, judging from their entire performance in the course. A single bad mark in an otherwise consistent record will often be discounted.
What do I do if I have a question or concern about grades?
If the problem is an objective error, like points that were added up incorrectly or a part of your solution that was entirely overlooked, please post on Piazza to ask for the correction. If your post requires detailed explanation or advocacy beyond just pointing to the mistake, that requirement is a sign it is not an objective grading error.
For all other grading issues, please visit an instructor’s office hours.