> 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.
I suspect the opposite. As I don't have a coherent argument yet,
let me just list some random observations:
(1) In verification one often needs to deal with very large formulas
(say, 300 lines long), but not in mathematics.
(2) BDD's (binary decision diagrams) have revolutionized the
verification of certain kinds of systems, but do not seem to
have any impact on the formalization of "real mathematics".
(3) The mathematics needed in verification is usually very elementary,
eg, elementary graph theory. In fact, it is so elementary that
mathematicians have never found the need to formalize it!
(Eg, when I need some formal graph theory to verify distributed
algorithms, I couldn't find any.)
(4) In mathematics one is interested in the "basic ideas" behind a theory
and usually do not bother to work out all the gory details. But in
verification the "basic ideas" behind a program are usually not in
doubt at all; rather, one is interested in making sure that all the
gory details have been taken care of, because programs are to be
executed by dumb machines that blindly follow instructions.
(5) Many algorithms (eg, many mutual exclusion algorithms) that one feels
need to be verified are "tricky" but not "deep", in the sense that
one does not need any deep mathematics to verify them. On the other
hand, the kind of hand-waving arguments one finds in ordinary math
textbooks are just not rigorous enough to catch all bugs.
- Ching Tsun