Discussion
Quoras auras-tu 'chabat de platussar ?
ontouchstart: RIP: https://youtu.be/tAl6wzDTrJA
arn3n: Pardon if I’m dumb/missed something: Is Tony Hoare dead? I see no news anywhere.
spooneybarger: Yes. He died last week.
rvz: RIP Tony Hoare.Legendary Turing Award Winner.
butterisgood: Wikipedia seems to say he passed yesterday.
tibbar: That is the claim of the post. I also don't see confirmation elsewhere
nextos: There is very little information around, this is the most authoritative post I could find. There are some comments on X as well.According to this blogpost, he sadly passed away last Thursday, March 5th.
jlhawn: There were a few recent edits about this on Tony Hoar's Wikipedia page which were reverted because there was no substantial evidence: https://en.wikipedia.org/w/index.php?title=Tony_Hoare&action...
riazrizvi: "The null reference was my billion dollar mistake responsible for innumerable errors, vulnerabilities and system crashes" (paraphrasing). I don't know. This design choice exposed the developer to system realities, and modern language approaches are based on decades of attempts to improve on it, and they are not necessarily better. Safer yes, but more weighty.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?
wging: But there are no citations on any of the edits claiming this, and there were two incompatible dates claimed (March 5, March 8).
fidotron: The confusion is possibly almost appropriate, given so much of his work was on creating systems which avoid confusion through using proper synchronized communication channels. The null pointer stuff is famous, but it's occam and the Communicating Sequential Processes work that were brilliant. Maybe it's also brilliantly wrong, as I think Actor model people could argue, but it is brilliant.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.
nextos: CSP and Hoare logic were brilliant. He was a huge proponent of formal methods.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.
cyberax: Some kind of an optional/variant type, enforced by the type system.
p1necone: Or if even that feels too verbose, just a 'nullable' modifier on the variable or field definition, with the default being not nullable.(Although Optional/Maybe types are definitely my preference based on the languages I've used)
reenorap: Once verified, I definitely think the creator of Quicksort deserves a black bar.
jonstewart: Yes, make it black.
hinkley: @dang is there such a thing as a double black bar? Because we need one for Tony.
toomuchtodo: Tags do nothing, email the mods if desired. Bottom bar has deets (“contact”).
behehebd: Any link to information?
spooneybarger: Came through personal contact who is close to the family.
nextos: It was edited again a few minutes ago and now displays Sunday, March 8th as his date of death.
codethief: And it's gone again!
jacquesm: It goes a lot further than Quicksort.
csb6: 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.
hinkley: 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.
jacquesm: And here we are throwing all that brilliance away with Async abominations. Software can be so simple and elegant.
magarnicle: "The problem isn't the concept of 'null', but rather that everything can be null, which makes it impossible to distinguish between the cases where null is an appropriate and expected value, from the cases where null is a defect."https://blog.ploeh.dk/2015/04/13/less-is-more-language-featu...
mynegation: Sir Tony Hoare visited Institute for System Programming in Moscow and gave a lecture quarter of the century ago. It was unforgettable experience to see the living legend of your field. He was a senior person then already and today I am going to celebrate his long and wonderful life.
intuitionist: Sadly it seems to be true. Heard it late last week from a coworker in a position to know.
eru: Actor model would also be brilliantly wrong: it doesn't compose smaller correct systems into larger correct systems.(Software) Transactional Memory and other ideas inspired by databases have a much better shot at this.
susam: I first stumbled upon Tony Hoare about 24 years ago while learning C from the book The C Programming Language by Kernighan and Richie. Quoting the relevant text:> 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 perhaps the first 'serious' algorithm I learnt to code myself. Thanks to K&R and Hoare for having a profound impact on my life.
laurieg: I saw a casual lecture given by Tony Hoare as a teenager. The atmosphere was warm and welcoming, even if I didn't fully understand all of the content. I remember he was very kind and answered my simple questions politely.
tombert: Damn.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.
dboreham: When I met him unfortunately I didn't realize how important he was (1987). The place where I worked used formal methods to verify the design of an FPU, in collaboration with the PRG. iirc the project was a success. I never heard of formal methods being successfully used again until TLA+ a few years ago.
fanf2: [delayed]
godd2: What is a black bar?
john_strinlai: when a significant figure in the tech/science community dies, hn will sometimes place a thin black bar at the top of the page in memoriam
EdNutting: Inmos’ Occam-based verification of their FPU in collaboration with researchers at Bristol and Oxford iirc? Citation: http://people.cs.bris.ac.uk/~dave/formalmethods.pdfDavid 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.
EdNutting: This post appears to have been hidden from the front page of HN?
EdNutting: “Inspired by” is an understatement of the century lol. David May and Sir Tony worked very closely together to enable the architecture to be as pure a runtime for CSP as you could get - at least in early versions of the architecture and accompanying Occam language. It expanded and deviated a bit later on iirc.Source: David loved to tell some of these stories to us as students at Bristol.
EdNutting: It’s also worth highlighting that the mathematical purity of the designs were also partly the problem with them. As a field, we’re still developing the maths of Effects and Effectful Algebras that are needed to make these systems both mathematically ‘pure’ (or at least sound to within some boundary) and ALSO capable of interfacing to the real world.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).
