I try to imagine using Coq to implement large and complicated software with specifications and proof. However, the manual work of writing proof is daunting. As a Coq newbie, to specify an insertion sort algorithm costs me a week and nearly one thousand lines accounting for specifications and proof.

Is there possibly to relieve the developer's burden and make computer prove arbitrary theorem, which is much stronger than 'auto' tactic? If not, what is the unsolved question in it?


closed as off-topic by cody, Andrej Bauer, András Salamon, Ryan Williams, Lev Reyzin Aug 18 '15 at 21:04

This question appears to be off-topic. The users who voted to close gave this specific reason:

  • "Your question does not appear to be a research-level question in theoretical computer science. For more information about the scope, please see help center. Your question might be suitable for Computer Science which has a broader scope." – cody, Andrej Bauer, András Salamon, Ryan Williams, Lev Reyzin
If this question can be reworded to fit the rules in the help center, please edit the question.

  • $\begingroup$ why3 can be used to generate proof obligations and feed them to various automated provers like Z3 or Yices. $\endgroup$ – max taldykin Jul 31 '15 at 6:15
  • 6
    $\begingroup$ Entscheidungsproblem! $\endgroup$ – Martin Berger Jul 31 '15 at 8:40

I guess the resource you are looking for is Adam Chlipala's Certified Programming with Dependent Types in which he builds up powerful tactics.


Not the answer you're looking for? Browse other questions tagged or ask your own question.