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.

Almost all of the earliest cited works on concurrency management in software were authored by C A R 'Tony' Hoare.

I genuinely forget he authored quicksort on the regular.

Actually, thanks to AI, this may change soon! we may be in a place where widespread formal verification is finally possible.