Editing QED manifesto (section)

==Further reading==
* [[H. Barendregt]] & F. Wiedijk, ''[https://www.cs.ru.nl/~freek/notes/RSpaper.pdf The Challenge of Computer Mathematics]'', Transactions A of the Royal Society 363 no. 1835, 2351–2375, 2005
*{{cite web|title=A Special Issue on Formal Proof|url=https://www.ams.org/notices/200811/|work=Notices of the American Mathematical Society|date=December 2008}} (open access issue)
* [[Richard DeMillo|Richard A. De Millo]], [[Richard J. Lipton]], [[Alan J. Perlis]], ''[http://www1.cs.columbia.edu/~angelos/Misc/p271-de_millo.pdf Social processes and proofs of theorems and programs]'', ''[[Communications of the ACM]]'', Volume 22, Issue 5  (May 1979), Pages: 271 - 280<!-- this paper is actually more relevant today for its comments on mathematical proofs rather than its (doomsday) predictions on the failure of program verification -->
* John Harrison, ''[http://www.cl.cam.ac.uk/~jrh13/papers/form-math3.html Formalized Mathematics]'', Technical Report 36, [[Turku Centre for Computer Science]] (TUCS)
* Ittay Weiss, ''[http://www.jsoftware.us/vol11/185-ID55.pdf The QED Manifesto after Two Decades  Version 2.0]'', ''Journal of Software'' vol. 11, no. 8, pp. 803-815, 2016.