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.