The “Debate” about Program Verif and the Lipton-Demillo-Perlis Paper (2021)(blog.computationalcomplexity.org)
blog.computationalcomplexity.org
The “Debate” about Program Verif and the Lipton-Demillo-Perlis Paper (2021)
https://blog.computationalcomplexity.org/2021/06/i-went-to-debate-about-program-verif.html
2 comments
Interesting considering formal verification is often pointed to as the only solution to understand all possible failure modes.
Reading this is sobering because I (ignorantly) assumed the only obstacle to success in formal verification was complexity (and the cost of complexity and few people able to do it).
Reading this is sobering because I (ignorantly) assumed the only obstacle to success in formal verification was complexity (and the cost of complexity and few people able to do it).
More important, everyone should read the paper being debated: Social Processes and Proofs of Theorems and Programs, Richard A. De Millo (Georgia Institute of Technology) and Richard J. Lipton and Alan J. Perlis (Yale University). This is one of my favorite CS papers because it exposes a lot of the mechanism behind making proofs that are convincing. What does it mean to say you have proven something.