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!