I agree. It seems to me that making formal systems easier to use
should be the main objective in verification research, if not QED. In
my experience the formalization of mathematics is not difficult. It
is the lack of automated reasoning power that makes verification
systems hard to use. Things that are obvious to people are just not
obvious to the machine and people hate having to prove extremely
obvious statements.
I don't know of any papers published by system designers where an
important theorem about an inference mechanism, like a completeness
theorem, has been machine verified before publication. If we, the
most expert users, don't use them in our own mathematics how can we
expect other less formally oriented mathematicians to use them? I
think we have a long way to go.
Shouldn't the QED community pay more attention to other potential
customers? Especially those who can PAY for it?
The main source of economic support seems to come from applications to
hardware and software verification. I suspect that the impediments to
practical verification in engineering are very similar to the
impediments to practical verification in mathematics.
David