249 points by nextos 16 hours ago | 61 comments
That was 35ish years ago. I just pulled up the paper now and I can't read the notation anymore... This might be something that I try applying an AI to. Get it to walk me through a paper paragraph-by-paragraph until I get back up to speed.
Retrospective: An Axiomatic Basis For Computer Programming. This was written 30 years after An Axiomatic Basis for Computer Programming to take stock on what was proven right and what was proven wrong - https://cacm.acm.org/opinion/retrospective-an-axiomatic-basi...
How Did Software Get So Reliable Without Proof? More detailed paper on the above theme (pdf) - https://6826.csail.mit.edu/2020/papers/noproof.pdf
I can't remember what Oxford did to resolve this, but I think they settled on `C.A.R. Hoare Residence`.
[1] https://www.cs.ox.ac.uk/people/jennifer.watson/tonyhoare.htm...
RIP Sir Tony.
Mr. Hoare did a talk back during my undergrad and for some reason despite totally checked out of school I attended, and it is one of my formative experiences. AFAICR it was about proving program correctness.
After it finished during the Q&A segment, one student asked him about his opinions about the famous Brooks essay No Silver Bullet and Mr. Hoare's answer was... total confusion. Apparently he had not heard of the concept at all! It could be a lost in translation thing but I don't think so since I remember understanding the phrase "silver bullet" which did not make any sense to me. And now Mr. Hoare and Dr. Brooks are two of my all time computing heroes.
Sad to think that the TonyHoare process has reached STOP.
RIP.
Turing Award Legend.
"A consequence of this principle is that every occurrence of every subscript of every subscripted variable was on every occasion checked at run time against both the upper and the lower declared bounds of the array. Many years later we asked our customers whether they wished us to provide an option to switch off these checks in the interests of efficiency on production runs. Unanimously, they urged us not to they already knew how frequently subscript errors occur on production runs where failure to detect them could be disastrous. I note with fear and horror that even in 1980 language designers and users have not learned this lesson. In any respectable branch of engineering, failure to observe such elementary precautions would have long been against the law."
-- C.A.R Hoare's "The 1980 ACM Turing Award Lecture"
If I remember correctly he has two ideas, his first was bubble sort, the second was quicksort.
He was already quite frail by then, yet clarity of mind undiminished. What came across in that talk, in addition to his technical material was his humor and warmth.
(Source: TFA)
I think about this a lot because it’s true of any complex system or argument, not just software.
> The first method is far more difficult. It demands the same skill, devotion, insight, and even inspiration as the discovery of the simple physical laws which underlie the complex phenomena of nature. It also requires a willingness to accept objectives which are limited by physical, logical, and technological constraints, and to accept a compromise when conflicting objectives cannot be met. No committee will ever do this until it is too late.
(All from his Turing Award lecture, "The Emperor's Old Clothes": https://www.labouseur.com/projects/codeReckon/papers/The-Emp...)
Cancer had snuck up on Dijkstra and there was not much time.
One senior professor who was helping out with this, asked him what is to be done with the correspondences. The professor, quite renowned himself, relates that Dijsktra tells him to keep the ones with "Tony" and throw the rest.
The professor adds with a dry wit, that his own correspondence with Dijsktra were in the pile too.
His presentation on his billion dollar mistake is something I still regularly share as a fervent believer that using null is an anti-pattern in _most_ cases. https://www.infoq.com/presentations/Null-References-The-Bill...
That said, his contributions greatly outweigh this 'mistake'.
As a non-junior dev I realize how stupid that was.
Somebody needs to contact ACM and have them make the above book freely available now; there can be no better epitaph.
Review of the above book - https://www.researchgate.net/publication/365933441_Review_on...
2) Tony Hoare's lecture in honour of Edsger Dijkstra (2010); What can we learn from Edsger W. Dijkstra? - https://www.cs.utexas.edu/~EWD/DijkstraMemorialLectures/Tony...
Somebody needs to now write a similar one for Hoare.
Truly one of the absolute greats in the history of Computer Science.
he read the algol 60 report (Naur, McCarthy, Perlis, …)
and that described "recursion"
=> aaah!
arch_deluxe•1h ago
baruchel•1h ago
rramadass•34m ago
Hoare Logic - https://en.wikipedia.org/wiki/Hoare_logic
lkuty•10m ago
wood_spirit•1h ago
His “billion dollar mistake”:
https://www.infoq.com/presentations/Null-References-The-Bill...
adrian_b•45m ago
Optional types were a very valuable invention and the fact that null values have been handled incorrectly in many programming languages or environments is not Hoare's fault.
Milpotel•45m ago
embit•1h ago
znpy•27m ago
there was a time, 10-15 years ago, when they were super cool. at some point they """diluted""" the technicality content and the nature of guests and they vanished into irrelevance.
madsohm•56m ago
adrian_b•48m ago
However, they were not just concurrent, but also communicating.
adrian_b•51m ago
Several keywords used in many programming languages come from Hoare, who either coined them himself, or he took them from another source, but all later programming language designers took them from Hoare. For example "case", but here only the keyword comes from Hoare, because a better form of the "case" statement had been proposed first by McCarthy many years earlier, under the name "select".
Another example is "class" which Simula 67, then all object-oriented languages took from Hoare, However, in this case the keyword has not been used first by Hoare, because he took "class", together with "record", from COBOL.
Another keyword popularized by Hoare is "new" (which Hoare took from Wirth, but everybody else took from Hoare), later used by many languages, including C++. At Hoare, the counterpart of "new" was "destroy", hence the name "destructor", used first in C++.
The paper "Record Handling", published by C.A.R. Hoare in 1965-11 was a major influence on many programming languages. It determined significant changes in the IBM PL/I programming language, including the introduction of pointers . It also was the source of many features of the SIMULA 67 and ALGOL 68 languages, from where they spread in many later programming languages.
The programming language "Occam" has been designed mainly as an implementation of the ideas described by Hoare in the "Communicating Sequential Processes" paper published in 1978-08. OpenMP also inherits many of those concepts, and some of them are also in CUDA.