Welcome to the EECS 755 blog for Spring 2024. You will find late-breaking information about the class and associated projects and exams here. The blog is available via RSS feed if you use an RSS aggregator.
Please keep in mind that this is a math class. We will treat programs as mathematical objects and we will be doing proofs from day one. Our proofs are done in an automated checker built into an IDE, but they are still proofs. We will move quickly and I expect you to install new software, correct syntax problems, and debug code on your own. I will teach you new material you need to know, but we don’t have time for extensive review of prerequisite material.
As you’re getting started it would be a good idea to install Coq on your system of choice. It is strongly suggested that you start with CoqIDE or VSCode. CoqIDE provides a drag-and-drop installation as well as an IDE for Coq. It is the simplest way to get started. VSCode with VSCoq is a far more powerful development environment that requires a bit more heavy lifting to install. Definitely worth the effort. If you are an emacs and linux user then ProofGeneral is a great option. I suspect far more of you use VSCode these days than emacs.
For reference, I am an emacs/ProofGeneral user while most of my students are VSCode users. While this prompts many spirited discussions in the lab, both work quite well.