The midterm exam will be automatically posted to the Canvas site at 2:30 this afternoon with a 24-hour window to complete it. I will be on an airplane headed home, but I will do my best to monitor and fix anything if something goes wrong.
Good luck everyone!
The formatting issue with Project 2 has been fixed. The {{ }} notation used
for Hoare triples was being interpreted as Jekyll/Liquid template expressions,
causing them to be stripped from the rendered page. The fix was to wrap code
blocks containing Hoare triples in Liquid raw tags, which tells Jekyll to treat
the enclosed content as literal text rather than template expressions.
The Project 2 page should now display all exercises correctly. No need to download the Markdown source anymore.
Thank you Claude.
I’ve run into some formatting issues for the project and class notes. Turns out that `` is both a Hoare Triple in Rocq style and the format for a Jekyll expression. My GitHub pages workflow uses Jekyll and is treating Hoare Triples as Jekyll declarations. Sorry about that.
Thankfully raw Markdown is easy to read. Here are links to compressed sources for the offending pages:
I will find a fix for this, but downloading the Markdown source is a good interim solution and will allow you to continue working.
Immediately after class I found the notes that I lost. They were, um, on my computer. Forgot to refresh an editor window. Regardless, I just pushed updated notes that include what I presented today.
I have the notes that I’m using in class available on the class website. Follow
the Formatted Lecture Notes link to get a formatted version. If you want to
download the unprocessed markdown file I use in Marp you can get that at
Unformatted Lecture Notes. Both links will usually get updated
before class. Note that the unformatted notes are zipped. gh-pages trys to
turn anything with an md extension into an html file.
Welcome to the EECS 762 blog. I will post information about projects, lectures and music here. Please check here often when projects are due as I will post late-breaking information including hints and corrections. Please see the course homepage for lecture topics, project postings and exam information as well as course administrative details.
To prepare for the course you should install Rocq and download the first two books, Logical Foundations and Programming Language Foundations, from the Software Foundations book series. We will start off with a quick review and jump quickly into IMP verification.
If you are not familiar with Rocq and IMP already, you can still be successful in the course. We will work together on projects in class early in the semester. This joint work will help you come up to speed quickly.
Some notes on installing Rocq from Will Thomas, my TA last semester:
opam installed (and properly initialized), just run opam install coq.9.0.0opam support for Windows natively is very new and relatively buggy. You might find yourself up against cases of “sorry you just can’t do that on Windows with opam currently”wsl
Navigate to some folder you care about putting the Rocq code in:
cd ~/Rocq/2025/lf # navigate to folder
code . # Launches vscode
From there, make sure you have the right Rocq extension installed (see below)
Use VSCode… alternatives exist, but they are not well-supported or have hardly any features.
In particular, I use the coq-lsp vscode extension.
Others also have great success with vsrocq.
Both will involve you using opam to install a language server. Thus, the importance of using opam.
Try searching online, it might be a common issue with a fix. Otherwise, come to office hours.