upvote

points

by tombert21 hours ago |
comments
upvoteby jballanc20 hours ago|
next
[-]
You can always check his entry on the Mathematics Genealogy Project: https://mathgenealogy.org/id.php?id=45760
reply
upvoteby tombert19 hours ago|
parent|
[-]
I actually knew about that, but it says "advisor unknown".

Regardless, he certainly knew Tony Hoare, and spoke extremely highly of him.

reply
upvoteby gjm1113 minutes ago|
parent|
[-]
You've probably tried this already, but just in case: If you can find a copy of his PhD thesis it's likely (or at least would be likely without the information that you've had trouble tracking down his advisor) to have some mention of his advisor's name in it.
reply
upvoteby dboreham20 hours ago|
prev|
[-]
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.
reply
upvoteby EdNutting20 hours ago|
parent|
next
[-]
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.pdf

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.

reply
upvoteby tombert5 hours ago|
parent|
[-]
I actually had two PhD advisors [1]; Jim Woodcock and Simon Foster.

Both of them are legitimately wonderful and intelligent humans that I can only use positive adjectives to describe, but the one I was referring to in this was Jim Woodcock [2]. He had many, many nice things to say about Tony Hoare.

[1] Just so I'm not misleading people, I didn't finish my PhD. No fault at all of the advisor or the school.

[2] https://en.wikipedia.org/wiki/Jim_Woodcock

reply
upvoteby fanf220 hours ago|
parent|
prev|
[-]
Inmos? Transputers were inspired by Hoare’s CSP.
reply
upvoteby EdNutting20 hours ago|
parent|
next
[-]
“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.

reply
upvoteby EdNutting20 hours ago|
parent|
next
[-]
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).

reply
upvoteby EdNutting20 hours ago|
parent|
prev|
[-]
Further Reading for the curious:

On specifically the relationship between Occam and Transputer architecture: http://people.cs.bris.ac.uk/~dave/transputer1984.pdf

Wider reading: http://people.cs.bris.ac.uk/~dave

reply