First Week Update

The first week of classes is underway! Here are a few important updates and reminders:

Getting Started with Coq

Make sure you have Coq (now called Rocq) installed and working. You can use:

• VSCode with the Coq extension (recommended for our lab)
• CoqIDE for a standalone interface
• ProofGeneral with Emacs if you prefer that environment

First Assignment

The first homework assignment covering Basics.v and BasicsTest.v is tentatively assigned Monday, August 25th. Remember:

• You need to complete 2/3 of the available points
• Include at least two 3-star or higher problems
• Submit your updated Basics.v file through Canvas

Office Hours Reminder

Don’t forget that office hours are MW 2:50-4:00 in 3048 Eaton Hall, or by appointment. Please don’t hesitate to come by if you’re having trouble with the proof system or course concepts.

Good luck with your first week!

In fact a proven truth, to be precise, is not a truth at all - it’s just the sum of proofs. ~Joseph Brodsky, Homage to Yalta