The Nature of Proof (2011)

> At one extreme lies the systems of formal proofs that encode proofs and theorems in an almost unrecognisable language “known only to a bunch of monks that live on a mountain"

I haven't read too far but I think this refers to the "classic" perspective on proofs which described in "Social Processes and Proofs of Theorems and Programs" [1]. The idea being that proofs should be derivable from first principles even if they are not in practice. This is in contrast to the "probabilistic" perspective which supposes that proofs are only ever "likely" to be correct.

I do a fair amount of work in Coq now and I've done extensive (first order logic) hand written proofs for the same material. So I guess I fall in to the classicist camp. There are a few things I like about this approach as I've experienced it:

Obviously there is no doubt about whether I've proven something. Or at worst there is an absolute minimum of doubt (down to the trusted computing base of Coq and CoC).

With a proof assistant I can easily play with my proof environment and try things out in the same way I do when I'm programming. I suppose this might also be true for more informal proofs but Proof General [2] makes it easy and enjoyable.

Most importantly, I can provide my encodings and proofs as a "library" that others can consume. At first glance this seems to have nothing to do with a classical view of proofs if they exist on paper, but I find higher level proof descriptions in papers hard to consume. Even when the proofs are in my area of expertise. Reading the mathematics fully laid out can be tedious but it contains all the answers to any questions you might have which can't always be said of more informal proofs.

To be fair, my area of expertise (PL) has extensive existing work in Coq and the tool works really well with these kinds of large but "shallow" proofs.

1. https://d1b10bmlvqabco.cloudfront.net/attach/ixkltd3cjy12bv/...

2. https://proofgeneral.github.io