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. He was right, just too early.

And here we are throwing all that brilliance away with Async abominations. Software can be so simple and elegant.

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.