The Coq mailing list

[Arnaud Spiwack <aspiwack AT lix.polytechnique.fr>]

I don't know about consensus, but I _often_ use the proof mechanism for
defining functions involving dependent types or contradictions.  Only in a
very few cases has the extraction suffered enough to force me to rewrite the
proof term manually.

For the records, writing programs by tactics was one the original motivations which led me to rewrite the tactic engine to allow for dependent subgoals (aka "true refine").