Sad that his (and many others') dream of widespread formal verification of software never came true. He made really fundamental contributions to computer science but will probably be mostly known for quicksort and the quote about his "billion dollar mistake", not his decades-long program to make formal methods more tractable.

Makes me think of an anecdote where Dijkstra said that he feared he would only be remembered for his shortest path algorithm.