Thursday, 20 November 2014

What's a proof good for?

Reading "Weird Machines" [1] a paragraph jumped out:
Following [2], we distinguish between formal proofs and the forms of mathematical reasoning de-facto communicated, discussed, and checked as proofs by the community of practicing mathematicians. The authors observe that a long string of formal deductions is nearly useless for establishing believability in a theorem, no matter how important, until it can be condensed, communicated, and verified by the mathematical community. The authors of [2] extended this community approach to validation of software—which, ironically, the hacker research community approaches rather closely in its modus operandi, as we will explain. 
It indicates that people don't care for proof as much as they should. More chillingly it highlights how much people are driven by emotion versus reason. So, [2] quickly jumped in priority of papers to read for me.

[1] Sergey Bratus, Michael E. Locasto, Meredith L. Patterson, Len Sassaman, and Anna Shubina, "From Buffer Overflows to "Weird Machines" and Theory of Computation,"

[2] Richard A. DeMillo, Richard J. Lipton, and Alan J. Perlis, “Social Processes and Proofs of Theorems and Programs,” technical report, Georgia Institute of Technology, Yale University, 1982: