Formal Proof – Theory and Practice, by John Harrison
Among the four articles on formal proofs in the Notices this is the one I enjoyed most.
John Harrison is the creator of HOL Light, one of the systems for doing formalized mathematics. He got hired by Intel in 1998 after the famous Pentium bug to work on formal verification of algorithms used in Intel chips (AMD hired David Russinoff). Harrison was one of the first people in Western Europe working in formal verification who noticed the value of Mizar’s declarative formal proof style and the existence of Mizar itself. He is a living example that formalized mathematics is relevant now and you can even earn living doing it if you a lucky genius.
I found some paragraphs of the “theory” part a bit too basic. I think explaining that
for example as we write “x+y” to denote mathematical object “x plus y“, we can use
to denote the proposition “p and q“
is not needed for the readers of Notices of American Mathematical Society. This stuff is taught in some high schools.
Formalized Mathematics 