Very amusing: "Given the small probability of successin attacking the sociological, cultural, and psychological causes of the quality controlproblem, it is nat

Very amusing: "Given the small probability of successin attacking the sociological, cultural, and psychological causes of the quality controlproblem, it is natural to look for a high-tech fix. After all, computers have so often cometo rescue us from the consequences of warped incentives and human laziness, carelessness,and incompetence. We’ve seen how computers have reversed the decline of K-12 educationin America, online instruction has turned undergraduates into hard-working and creativelearners, the information superhighway has reduced inequality between the rich and poorand between the Global North and Global South, smart appliances will solve the energyproblem and bring global warming to a halt, and social media and the internet havestrengthened American democracy and prevented the election of demagogues, liars, andbigots. By the same token it stands to reason that computer-generated proofs will removehuman error from provable security papers. At least that’s how it looked twelve yearsago when the first author wrote the first of two papers [221, 222] critiquing automatedtheorem-proving."