Prof. Michael J. C. Gordon, FRS was a great pioneer in both computer-aided formal verification and interactive theorem proving. His own work and that of his students helped to explore and map out these new fields and in particular the fruitful connections between them. His seminal HOL theorem prover not only gave rise to many successors and relatives, but was also the framework in which many new ideas and techniques in theorem proving and verification were explored for the first time. Mike's untimely death in August 2017 was a tragedy first and foremost for his family, but was felt as a shocking loss too by many of us who felt part of his extended family of friends, former students and colleagues throughout the world. Mike's intellectual example as well as his unassuming nature and personal kindness will always be something we treasure. In my talk here I will present an overall perspective on Mike's life and the whole arc of his intellectual career. I will also spend  time looking ahead, for the research themes he helped to establish are still vital and exciting today in both academia and industry.