Comment by nimih

On the subject of the tail wagging the dog, mathematicians have been fighting about non-constructive proofs and the law of excluded middle far longer than they've been writing proof assistants, and deriding a direction of active and fruitful research just because you're not personally interested in it seems rather myopic.