My favourite quote of his is “There are two ways of constructing a piece of software: One is to make it so simple that there are obviously no errors, and the other is to make it so complicated that there are no obvious errors.”
While we hope it's not true, if it is a very deserved RIP.
He famously gave up on making formal methods mainstream, but I believe there will be a comeback quite soon.
On generated code, verification is the bottleneck. He was right, just too early.
(Software) Transactional Memory and other ideas inspired by databases have a much better shot at this.
Tony Hoare was on my bucket list of people I wanted to meet before I or they die. My grad school advisor always talked of him extremely highly, and while I cannot seem to confirm it, I believe Hoare might have been his PhD advisor.
It's hard to overstate how important Hoare was. CSP and Hoare Logic and UTP are all basically entire fields in their own right. It makes me sad he's gone.
David May was my PhD supervisor and always spoke very highly of Sir Tony Hoare.
Edit: I’m also lucky enough to have worked with Geoff Barrett, the guy that completed that formal verification (and went on to do numerous other interesting things). Some people may be interested to learn that this work was the very first formal verification of an FPU - and the famous Intel FPU bug could have been avoided had Intel been using the verification methods that the Inmos and University teams pioneered.
Source: David loved to tell some of these stories to us as students at Bristol.
Transputer and Occam were, in this sense, too early. A rebuild now combining more recent developments from Effect Algebras would be very interesting technically. (Commercially there are all sorts of barriers).
Makes me think of an anecdote where Dijkstra said that he feared he would only be remembered for his shortest path algorithm.
I genuinely forget he authored quicksort on the regular.
> Another good example of recursion is quicksort, a sorting algorithm developed by C.A.R. Hoare in 1962. Given an array, one element is chosen and the others partitioned in two subsets - those less than the partition element and those greater than or equal to it. The same process is then applied recursively to the two subsets. When a subset has fewer than two elements, it doesn't need any sorting; this stops the recursion.
> Our version of quicksort is not the fastest possible, but it's one of the simplest. We use the middle element of each subarray for partitioning. [...]
It was one of the first few 'serious' algorithms I learnt to implement on my own. More generally, the book had a profound impact on my life. It made me fall in love with computer programming and ultimately choose it as my career. Thanks to K&R, Tony Hoare and the many other giants on whose shoulders I stand.
> Jonathan Bowen informed me of Tony Hoare's death on Thursday, March 5th. (translated from French)
The main reason to find it surprising is that it's now 4 days since then, I'd have expected something to have been published besides this page.According to this blogpost, he sadly passed away last Thursday, March 5th.
Legendary Turing Award Winner.
Can anyone suggest a better approach for a situation like this in the future? What's better than exposing addressing the problem with a light solution?
https://blog.ploeh.dk/2015/04/13/less-is-more-language-featu...
(Although Optional/Maybe types are definitely my preference based on the languages I've used)
RIP good sir