For those who prefer the original format: <a href="https://www.cs.utexas.edu/users/EWD/ewd08xx/EWD841.PDF" rel="nofollow">https://www.cs.utexas.edu/users/EWD/ewd08xx/EWD841.PDF</a><p>Interesting surprise encountering Margaret Hamilton's name in there.<p>My comment on pg's <i>Succinctness is Power</i> echoes some of the things Dijkstra says in here, though I wasn't talking about proof assistants, just a more informal notion of errors and problems: <a href="http://www.paulgraham.com/redund.html" rel="nofollow">http://www.paulgraham.com/redund.html</a>
I first came across this quote funnily by a book that is called The Royal Road to Algebraic Geometry.<p><a href="https://link.springer.com/book/10.1007/978-3-642-19225-8" rel="nofollow">https://link.springer.com/book/10.1007/978-3-642-19225-8</a>