On making mathematic proof a business
Byron Cook (Amazon | AWS)
Distinguished Lecture
Thursday, October 12, 2023, 3:30 pm
Abstract
With only a few niche exceptions, the software industry has previously never made deep use of mechanized proof search in mathematical logic (a.k.a. Automated Reasoning). At Amazon we have recently seen tremendous adoption of the approach by product groups. Amazon’s use ranges from customer-facing launches to internal proof-based projects. This talk describes those projects, and tries to capture aspects of why Amazon has found the approach so useful where others have not. The talk also describes challenges that we face to scale the approach to the next level.
Bio
Dr. Byron Cook, FREng, is Professor of Computer Science at University College London (UCL). Byron is also Vice President and Distinguished Scientist at Amazon. From 2002-2014 Byron was at Microsoft Research. Byron's interests include computer/network security, program analysis/verification, programming languages, theorem proving, logic, hardware design, operating systems, and biological systems.
This talk is available on the Allen School's YouTube channel.