CSC535: Coq: Why Use Coq in This Course [19/21]

• Rigor
  • using Coq forces us to be completely precise about the things we define and the claims we make about them
  • Coq's core notions of inductive definition and proof are a good match for the fundamental ways we define and reason about programming languages
• Interactivity
  • Instant feedback on homework
  • Easy to experiment with consequences of changing definitions, different reasoning techniques, etc.
• Useful background
  • Proof assistants are being used more and more widely in industry and academia
• Fun!