The Coq mailing list

[Dmitry Grebeniuk <gdsfh1 AT gmail.com>]

Hello.

> Arnaud, Thank you. The notion that it's reasonable to force one who wishes
> to program to "reprove" theorems with opaque proof terms makes sense, given
> that proofs are in general produced without regard for efficiency.

  But it's not efficient in sense of "time spent by programmer to 1.
determine which proofs are opaque, 2. prove it transparently".  For
example, I needed to compute with nat, plus and le, so I spent more
than an hour of my time to prove some facts about it.
  Imagine how much time I could spend if I had real numbers or
something non-trivial (even Z!).
  So I think it's completely not reasonable to force programmer to
"reprove" already proved things, if he's sure that execution time of
"Eval compute" doesn't matter compared to "reprove" time.