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