In this latest episode, we interview John Harrison, Senior Principal Applied Scientist with the AWS Automated Reasoning Group. John describes his experience helping to shape innovative applications of automated reasoning to pressing technology challenges. He talks about his time at Intel, how he transitioned from a research scientist to technology product teams, automated reasoning techniques that he has used in his career and at AWS, his theorem prover called HOL Light and his 702 page book, Handbook of Practical Logic and Automated Reasoning. Byron Cook, Director of the AWS Automated Reasoning Group, interviews John and will be featured throughout the miniseries. Byron is leading the provable security initiative at AWS, which is a collection of technologies that provide higher security assurance to customers by giving them a deeper understanding of their cloud architecture.