The Notices of the American Mathematical Society has published a special issue on “formal proof”, leading off with an article [pdf] on the where the field stands. I find this subject exciting because of its promise, not just as a tool in mathematics, but to solidify the foundations of the computational world.
Inference Rules in HOL [...]
