Michael J.C. Gordon FRS Professor of Computer Assisted Reasoning (28 February 1948–22 August 2017)
Formal Aspects of Computing · 2017
was a pioneer in the field of interactive theorem proving, with a focus on hardware verification. This field is concerned with certifying system designs by proving their correctness mathematically. Mike Gordon shaped this field from the beginning, demonstrating the feasibility of hardware verification on realworld computer designs. His students extended the work to such diverse areas as the verification of floating-point algorithms, the verification of probabilistic algorithms and the verified translation of source code to (necessarily correct) machine language code. In recognition of his achievements, he was elected to the Royal Society in 1994, and he continued to make valuable contributions until the end of his career.