Review: Social Processes and Proofs of Programs
High Level Summary
In this paper, De Millo, et al. criticize the idea of comparing program verification to mathematically proofs, and claim that it is unrealistic for verification to have the same importance in programming as proofs do in mathematics. They go into great depths and breadths to show that mathematical proofs are actually a social process, while verification is not. Verification is not fun to read, hard to understand, doesn't really provide programmers with confidence, and is unrealistic on complicated real-world systems.
I think the most insightful point of this paper is in its title, "social processes." It is indeed a key difference of proofs and verification, and the authors explain the difference with an abundance of stories and examples. Their point about how specifications, being informal and complex, play in the role of real-world programming is also a very strong point. Overall, these two points make the paper very convincing that at least in 1979, verification on real-world systems is not quite realistic. I also really enjoyed the debate across 30 years from the additional readings, especially how Asperti, et al. mimic De Millo, et al.'s style of putting a quote at the beginning of each section. Very flavorful.
While I think this paper is very insightful about both mathematics and programming, it is limited to its time of writing, which is 40 years ago. From the long thread of debated included in the reading list across 30 years, we can kind of see that De Millo, et al.'s argument is actually very controversial, and a bit outdated. Reality also showed that their bold predictions about verification were not quite accurate. Program verification has definitely been a hot area of research, and now many complex real-world systems are also verified, in contrast to De Millo, et al.'s predictions. Also, this seems to be a pretty lengthy paper to show the author's point. Although the many stories, examples and analogies are very educative, I had to take a nap after reading the paper. The sections are also way too long to appear organized. Their prediction about verification's future is also not very well-supported. It almost feels like the authors' opinion is too strong, and I feel that they could have put in a more calm and objective way.