Social processes and proofs of theorems and programs (1979) [pdf] | Hacker News Reader

Social processes and proofs of theorems and programs (1979) [pdf]

cs.umd.edu

18 pointsamadeuspagel7 comments

The paper argues against those who think that "programming should strive to be more mathematical" through the development and adoption of formal methods. It points out that "more mathematical" does not implicate formal methods, since proofs by mathematicians are informal and their correctness is established by social processes. The author fears that an over-emphasis on formal methods could stifle innovation (in particular, in programming language design).

As a mathematician that works with proof assistants, I largely agree with this thesis. However, I don't think there is any reason to have any such fears associated with formal methods. I think informal proofs, as the exist in both CS and maths, are here to stay. And, on the contrary, I think investigations into formal methods can drive new theory and insight. For example, one could say that the formal system of homotopy type theory (HoTT) is a programming language created in order to reason about highly "coherent" mathematical structures, which HoTT often does very well. In addition, being a formal system, HoTT is well-suited for formal methods -- but even so, many mathematicians still prefer to work informally in this language.

In summary, I think the article makes a valid point, but the motivating fears seems unfounded in retrospect.

The paper shows its age. A lot has happened since 1979. Projects like CompCert, seL4, Project Everest, Coq, Dafny, F* etc. shows what can be done with modern proof tools. And it is getting better every day.

And I will claim that “formal” proofs, as practiced today by most professional mathematicians, are basically just informal proofs with more details, reviewed by flawed humans in a social process. Nothing wrong with that of course! But just pointing out that it doesn’t reach the high level of confidence that modern proof tools can deliver.

The LEAN/mathlib project is an interesting example of what the future of truly formal mathematics might look like.

But "formal" proofs by proof systems are no less social processes. They are still developed by humans, require human agreement, and still have bugs.

I think the main "bug" in proof systems is thinking that they will or should replace humans, as in most tech development today, rather than supplementing human activity.

Nope. With proof systems you have to convince the software. With traditional mathematics you have to convince a group of peers.

Unless of course you consider interacting with software to be “social”.

I didn't say it was the same social social process but still a social process. Software is written by humans. Proof systems are not impervious to mistakes or issues. The point is that it is just another way to help augment normal proofs.

The writers of the proof systems need to convince themselves and others that they have imolemented and tested things properly. Someone writing a proof in such a system needs to convince others that they have translated the proof correctly and used the system appropriately.

For example, the below article describes a very social process to writing down a Lean proof of a theorem:

https://www.quantamagazine.org/lean-computer-program-confirm...

> Unless of course you consider interacting with software to be “social”.

Yes, but not in the way you imply. When you write software, you are writing for other humans and thus communicating to other humans. The fact that a computer can perform a task based upon what's written is basically just the cherry on top and not the whole cake.

Fields Medalist Peter Scholze does not agree with you:

https://www.microsoft.com/en-us/research/project/lean/

“Lean has already demonstrated its potential to revolutionise and radically accelerate mathematics, for example, helping Fields Medalist Peter Scholze confirm a new theorem in the Liquid Tensor Experiment.”

Social Processes and Proofs of Theorems and Programs (1979) [pdf] - https://news.ycombinator.com/item?id=16421444 - Feb 2018 (1 comment)

Reply on news.ycombinator.com