Comment by jgrahamc
11 hours ago
In the early eighties, for example, he brought to Oxford the creators of two major formal specification languages: Cliff Jones with VDM, Jean-Raymond Abrial with Z. At Oxford, Z actually underwent a systematic rework, reminiscent of the Goethe quip reproduced above, with Frenchmen and mathematicians replaced by English mathematicians (or computer scientists). The new version enjoyed immense success in Britain, won a Queen’s Award and was used not only academically but in many mission-critical applications in industry, leading to a number of startups and work by such researchers (all having gone through Oxford at some point) as Jim Woodcock, Carroll Morgan, Jim Davies, J. Michael Spivey, Ian Hayes and Ib Holm Sørensen.
This was the world I walked into in 1986 as an undergraduate studying Mathematics and Computation. I was quite quickly indoctrinated in the ways of Z notation [1] and CSP [2] and had to learn to program in ML. I still have all the lecture and class notes and they are quite fascinating to look at so many years later. Funny to read the names of celebrated researchers that I just thought of as "the person who teachers subject X". I do recall Carroll Morgan's teaching being very entertaining and interesting. And I interacted quite a bit with Jim Davies, Jim Woodcock and Mike Spivey.
Having decided I wanted to stay and do a DPhil I managed to get through the interview with Tony Hoare (hardest question: "Where else have you applied to study?" answer: "Nowhere, I want to stay here") and that led to my DPhil being all CSP and occam [3]. I seem to remember we had an array of 16(?) transputers [4] that the university had managed to get because of a manufacturing problem (I think the dies were incorrecty placed making the pinouts weird, but someone had made a custom PCB for it).
Imagine my delight when Go came around and I got to see CSP in a new language.
[1] https://en.wikipedia.org/wiki/Z_notation
[2] https://en.wikipedia.org/wiki/Communicating_sequential_proce...
[3] https://en.wikipedia.org/wiki/Occam_(programming_language)
These are all great contributions, I even briefly used Occam/Transputer.
Most however will be most familiar with Quicksort[0] and NULL.
[0] https://en.wikipedia.org/wiki/Quicksort
I can only imagine what it must've been like throughout the 90s and teens seeing people whack their heads against concurrency.
Well, of course, a lot had already been done by the time I got there. But what really struck me about CSP was how easy it was to reason about concurrent programs because synchronization and communication were the same thing. In my doctoral thesis I created a provably secure multi-user file systems which went from specification to CSP to occam.
It was not a fun time. In Java, for example, the concurrency & threading primitives were so low level it was almost impossible for anyone to use them and get it right. The concurrency package introduced in 2004 brought higher level concepts and mostly eliminated the need to risk the footguns present in the thread/runnable/synchronized constructs.
As far back at 1995 people were warning against using threads. See for example John Ousterhout's "Why Threads are a Bad Idea (for most purposes)" <https://blog.acolyer.org/2014/12/09/why-threads-are-a-bad-id...>
> In Java, for example, the concurrency & threading primitives were so low level it was almost impossible for anyone to use them and get it right.
I disagree with this. As long as you had an understanding of critical sections and notify & wait, typical use cases were reasonably straightforward. The issues were largely when you ventured outside of critical sections, or when you didn’t understand the extent of your shared mutable state that needed to be protected by critical sections (which would still be a problem today, for example when you move references to mutable objects between threads — the concurrent package doesn’t really help you there).
The problem with Java pre-1.5 was that the memory model wasn’t very well-defined outside of locks, and that the guarantees that were specified weren’t actually assured by most implementations [0]. That changed with the new memory model in Java 1.5, which also enabled important parts of the new concurrency package.
[0] https://www.cs.tufts.edu/~nr/cs257/archive/bill-pugh/jmm2.pd...
Now I see it written down I realize how lucky I've been to have spent time at the Programming Research Group at Oxford when Tony Hoare was running it and then to have worked for and founded a company with John Ousterhout. And, yeah, when I worked with him he wasn't a fan of threads.