General Information
Teaches formal verification through computer-assisted theorem proving using Coq. Take this class if you liked the unit on Coq in 3110 or if you like really cool programming languages or if you like logical reasoning. The class follows a textbook/workbook so it’s very, very easy to succeed without attending lecture, but you might still go because Professor Clarkson is great. The exams are the exact same format (write/prove some algorithms in Coq) as assigments. Plus, if Coq accepts your code, you know it is correct (which means you always know your score before you submit).
Prerequisites
3110
Topics Covered
Workload
Light to medium for an upper level class. Light if you just want a good grade, medium if you want to get everything perfect before you submit. Aprox weekly assigments, two prelims, and a final.
General Advice
-
Don’t just try random tactics to try and make your proof compile. On the other hand, sometimes random tactics lead to something that looks familiar and then you can come up with a proof from that.
-
Setting up your IDE/environment for this class can be really hard. Don’t feel stupid, it is actually hard.
Testimonials
Very interesting. I even excitedly told my friends about the textbook format, lol.
Makes you think that all other proofs are backwards.