Meeting | Monday/Thursday, 11:45AM-1:25PM, International Village 014 |
Instructor | Daniel Patterson ([email protected]) (WVH 308) |
Office Hours | Monday 3pm-4pm, Wednesday 11am-12pm outside WVH 308 |
“Can you trust your compiler?” — Xavier Leroy, developer of the Compcert verified C compiler
Software is written in a variety of languages, and in most cases, in order to run, it must be compiled down to some lower-level target. But what if that compiler isn’t correct? Compilers are some of the trickier pieces of software we build, and yet bugs in them are insidious: bugs in compilers mean that one of our most basic debugging strategies, reading source code, may not be helpful, since what actually ran may not correspond to that source code!
In the presence of buggy compilers, we must worry about what the compiler does and how our programs are translated to the target, possibly looking at compiler output or stepping through with low-level debuggers. Much better if the compiler were, essentially, invisible — if the source code fully specified what would happen. But a compiler can only truly be invisible if we can be sure that it does exactly what we expect: if we are sure it is correct. To be absolutely sure, we must prove it correct, and build a verified compiler.
The course will be highly collaborative, and light on lectures. An average class will involve some time to collectively work on questions that are brought up (before or at the beginning of class), a brief introduction to a problem (usually a proof), time to work on the problem in small groups, one group presenting their solution with feedback, and a brief summary of highlights, or any points missed. Please bring your laptop to class every day. (If you do not have a laptop, we’ll figure something out, contact me: [email protected]).
We will draw reading from multiple texts, all available online for free. The abbreviations here are used in the syllabus (this list may be extended throughout the semester):
PnP | Programs and Proofs | Ilya Sergey | https://ilyasergey.net/pnp/pnp.pdf |
MC | Mathematical Components | Assia Mahboubi and Enrico Tassi | https://math-comp.github.io/mcb/book.pdf |
LF/dbp | Logical Foundations, edited by me | Pierce et. al / Daniel Patterson | Linked below as needed |
PLF/dbp | Programming Language Foundations, edited by me | Pierce et. al / Daniel Patterson | Linked below as needed |
FRAP | Formal Reasoning About Programs | Adam Chlipala | http://adam.chlipala.net/frap/frap_book.pdf |
Week | Date | Reading | Topic | Assignment |
---|---|---|---|---|
0 | 9/5 | Course overview, Github setup, Coq setup. | 0 - due 9/12 | |
1 | 9/9 | PnP 2, MC 1 | Functional programming in Coq | |
9/12 | PnP 3.1-3.6 | Propositional logic and proofs | 1 - due 9/19 | |
2 | 9/16 | MC 2, PnP 3.7-3.8, 4.1-4.2 | Equality, rewriting | |
9/19 | MC 3 | Tactics & inductive proofs | 2 - due 9/26 | |
3 | 9/23 | PnP 4.3, 5, MC 4 | Views & boolean reflection | |
9/26 | PnP 6 | Structure of proofs | 3 - due 10/3 | |
4 | 9/30 | LF/dbp Imp | Big-step reduction & first compiler | |
10/3 | PLF/dbp Smallstep | Small-step operational semantics | 4 - due 10/10 | |
5 | 10/7 | FRAP 9.1 | Simulation arguments (see Template) | |
10/10 | FRAP 9.2-9.3 | Stuttering | 5 - due 10/17 | |
6 | 10/14 | NO CLASS | ||
10/17 | De Bruijn indices & eval contexts | 6 - due 10/24 | ||
7 | 10/21 | More about evaluation contexts | ||
10/24 | Tactic automation. | 7 - due 10/31 | ||
8 | 10/28 | IMP big step relational vs. fixpoint | ||
10/31 | IMP big step soundness | 8 - due 11/7 | ||
9 | 11/4 | IMP compiler 1 | ||
11/7 | IMP compiler 2 | 9 - due 11/14 | ||
10 | 11/11 | NO CLASS | ||
11/14 | Discuss adding language features | 10 - due 11/21 | ||
11 | 11/18 | Abstract interp const prop 1 | ||
11/21 | Abstract interp const prop 2 | 11 - due 12/2 | ||
12 | 11/25 | Abstract interp const prop 3 | ||
11/28 | NO CLASS | |||
13 | 12/2 | Extraction |
We will use three methods:
[email protected]
), which you should be on. If you are not enrolled in the class, but are participating (auditing, or something), please let me know and I’ll add you.Grades will be assigned as follows:
Class participation | 10% |
First 4 assignments | 2.5% each |
Last 8 assignments | 10% each |
All assignments should be committed to your private github repository (e.g., github.ccs.neu.edu/you/verifcomp
) (see Github setup for notes about setup; we will go over this in the first class). When you are ready to submit the assignment, make a comment in the corresponding assignment issue in the shared repository (github.ccs.neu.edu/verifcomp/19) with just the user/repo@sha
that corresponds to your submission (sha
is the commit hash of the revision with your submission. If you do work afterwards, for example on the next assignment, that’s fine, don’t worry about pushing because I will grade that particular revision). Comments have timestamps, so you can be sure that you have “turned the assignment in” before the deadline provided the timestamp is before the deadline. I will review and give you your grades via github on your private repository (it’ll happen via a pull request, as that’s the only mechanism that allows easy commenting on entire files, regardless of how many commits you made).
Assignments will have 10% deducted from the maximum total for every hour they are late, rounded up to the nearest hour. You will still get the same percentage of points, just against the smaller total. For example, if you got 80% of the points on an assignment, but you were 1hr late, you would get .8 * .9 = .72 of the points (not .8 - .1 = .7 total). However, you will be given 72 free late hours over the entire semester, which will be automatically optimally assigned (which means we will rank the hours late by how many points they lost you, and remove the top 72 of them). If you have an exceptional situation, please let me know – this policy is not set in stone, but is intended to balance progressing steadily through the course (and timely grading) with the inevitable minor things that come up.
Throughout the semester, there may be opportunities for earning bonus points. For any assignments that are turned in with Admitted
lemmas, I will anonymize the assignment, remove anything that is unnecessary for the lemma, and add it to the bonus
directory of the course repository. Each lemma will be given a point value – this is how many bonus points you will earn if you either prove the lemma or if you disprove it (i.e., if you can prove that assuming the lemma allows you to prove False
). If you have proved (or disproved) a lemma, open a pull request with the proof filled in. You might want to communicate on slack before starting on something to be sure someone else isn’t working on a lemma. Note that there is no reason why you can’t solve lemmas that you Admitted
yourself!
Collaboration on all aspects of the course (including assignments) is encouraged. However, if you do get help on an assignment, you must:
elim
).If you would like to audit the course, you are welcome to. Just let me know and I’ll get you on the course mailing list, slack, etc. You will be able to participate fully in the course, with two caveats:
What is class participation grading for?
The course is, by design, collaborative. This means, it needs everyone to participate. That means presenting solutions to in-class problems, contributing thoughts to questions that are brought up, sending in places you got stuck for us to work on in class, etc.
If I miss a class, can I still get a full class participation grade?
Missing a single class (or even two) won’t hurt your grade, provided you are participating the rest of the time. The grade is not about attendance. And indeed, if you attend every class but never speak, you will get a 0 (attending is not the same as participating).
Why are the early assignments worth so much less?
These assignments are about learning Coq, and a lot of the exercises are (unfortunately) easy to google for solutions to. Doing so will only hurt you (in addition to obviously being an academic code violation), as you won’t actually learn how to use Coq, but in an attempt to disincentivize doing so, I’m making the assignments not count that much towards your grade.
How will assignments be graded? What if I can’t figure a proof out? Will I get a zero?
Partial credit and partial proofs are completely accepted, and expected. The magnitude of what is Admitted
, will determine, of course, the extent of the partial credit, but certainly don’t think that just because you aren’t able to get everything to go through that you will get no credit. Also, as noted above, anything you admit you can potentially solve later for bonus points (but so, of course, can your classmates).
Will there be a final exam?
There will be no final exam. There will be no in-class exams, at all.
Please reach out to the instructor: Daniel Patterson ([email protected])