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?