Мартин Абади
Аргентинский учёный, сделавший протоколы безопасности предметом доказательств, а затем принёсший ту же строгость в машинное обучение.
BAN-логика (1989, с Майклом Барроузом и Роджером Нидемом) стала первым практичным формальным инструментом для рассуждений о том, во что вправе верить участники протокола аутентификации. Вместе с Эндрю Гордоном он в 1997 году разработал spi-исчисление, а вместе с Нидемом написал перечень разумных инженерных практик проектирования протоколов, который до сих пор ловит ошибки, ускользающие от формальных методов.
В 2005 году он с коллегами из Microsoft Research предложил целостность потока управления (control-flow integrity), теперь встроенную в компиляторы и процессоры. В Google он стал соавтором TensorFlow и метода дифференциально приватного глубокого обучения 2016 года. Мало кто так часто менял области, ни разу не уходя от вопроса, что система на самом деле гарантирует.