Here's what some students in the fall 2001 offering of cs745 had to say about whether they would recommend this course to other students:
Yes. Almost every grad student is going to suggest a new solution, idea, algorithm, etc. So they need to prove/verify the correctness of their idea. Formal methods is a powerful tool to do that.
Yes. Formal methods is a very important technique. Without learning it is like learning math without proof.
Yes, because verification techniques are becoming more and more important to software and hardware development.
Yes, this course covers a lot of logics, ... These are also the foundation for other theories, such as database theory.
Yes, it's a course that you can learn things that you didn't learn from an undergrad course, and that you might use in future work, especially for software engineering students.
And finally, the course seems to inspire some students to poetry:
Apologies to T.S. Geisel (Dr. Seuss) (credits to Kenn Heinrich)
> I am Sam. Sam I am.
> Will you prove my The-o-ram?
> Will you prove it with DISCH_TAC?
> Will you prove it front-to-back?
-
- Not with a SKOLEM!
- Not with an e!
- Not with a REWRITE!
- Let me be!
- I will not prove your The-o-ram
- I will not prove it, Sam-I-am!
-
- HOL ERR