• What is Coq?
• Did you really need to name it like that?
• Is Coq a theorem prover?
• What are the other theorem provers?
• What do I have to trust when I see a proof checked by Coq?
• Where can I find information about the theory behind Coq?
• How can I use Coq to prove programs?
• How old is Coq?
• What are the Coq-related tools?
• What are the high-level tactics of Coq?
• What are the main libraries available for Coq?
• What are the mathematical applications for Coq?
• What are the industrial applications for Coq?