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.

The core learning objectives for the class are to leave students able to:

1. In the language of formal logic, explain what it means for a program or its parts to be correct.  (These explanations are called specifications.)
2. 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.)
3. 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.)
4. Develop code in the particular verification-enabled programming language called Dafny, though the key takeaways apply more broadly.

In fact, we are designing this class 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 lectures).  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 (no group projects).  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 manage to skip covering systematic testing, a key topic from 6.102, because program verification is more comprehensive (if much less commonly used in industry today).

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.

Grading

We're keeping it simple in this experimental offering: your grade is entirely based on Dafny assignments (writing programs, including specifications and proofs).  Generally, one assignment releases each Wednesday and is due the following Wednesday.  Assignments are weighed equally in final grades.

Grading can be mostly automatic, based on which parts of a program you convinced Dafny are correct!

To keep things simple for students, we'll adopt the academic-integrity policy of our prerequisite 6.101.

Class Time

We have two lectures a week, plus one weekly recitation where the latest assignment will be presented with a chance for asking questions about it.

Lectures will be highly interactive, with an instructor driving a Dafny-programming session, using audience feedback to develop different programs that demonstrate major concepts we are teaching.  The code from each lecture will be posted on the web afterward.

Course Staff

Beyond Prof. Adam Chlipala, we're very lucky to have Dafny creator Dr. Rustan Leino as a coinstructor this term!  We also have three TAs with extensive experience in program verification.

You can contact the full staff at 6.s057-staff@mit.edu or just the instructors at 6.s057-instructors@mit.edu.  The latter address is more appropriate for administrative issues like extensions on assignments.

Generally, the best way to get help on assignments is to attend office hours in-person!  (The schedule will be posted soon.)  We will also start out trying to use the Canvas discussions system for written help, though, really, debugging code problems is a lot easier in-person.

References

We don't require a textbook, but Program Proofs by coinstructor Leino is a recommended source for a book-format introduction to Dafny.  We'll do our best to keep the commented lecture code and other files posted here sufficient for following along and completing all the assignments, but it'll definitely help to attend lecture, so you don't miss any helpful reinforcement of important ideas.

Enrollment Limit

To keep logistics simple while we somewhat empirically determine what works well in this new class and what doesn't, we will cap enrollment at 40 students.  Turning in the first homework assignment on-time will be the key signal that a student wishes to remain enrolled in the class!  If more than 40 people turn in that assignment, we will have to apply a procedure to decide who stays in the class, which will be based on a survey to gather important information, like on who will have trouble graduating on-time without this class.