There is no ‘royal road’ to geometry (1982)
cs.utexas.edu
cs.utexas.edu
Interesting surprise encountering Margaret Hamilton's name in there.
My comment on pg's Succinctness is Power 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: http://www.paulgraham.com/redund.html