In 1980, barely two years after Hoare's paper, Gerard Holzmann and Rob Pike created a protocol analyzer called pan that takes a CSP dialect as input. [...] Holzmann reports that βPan found its first error in a Bell Labs data-switch control protocol on 21 November 1980.β That dialect may well have been the first CSP language at Bell Labs, and it certainly provided Pike with experience using and implementing a CSP-like language, his first of many. [...] Holzmann's protocol analyzer developed into the Spin model checker and its Promela language.
How cool. Gerard (http://gerard.holzmann.usesthis.com) is now using Spin and several other verification tools to improve source code quality for space missions at JPL. I did not know about this connection of his work to CSP and, indirectly, to Go.
