Martín Abadi
Informático argentino que convirtió los protocolos de seguridad en algo sobre lo que se pueden demostrar cosas, y después llevó ese mismo rigor al aprendizaje automático.
La lógica BAN (1989, con Michael Burrows y Roger Needham) fue la primera herramienta formal práctica para razonar sobre lo que los participantes de un protocolo de autenticación tienen derecho a creer. Con Andrew Gordon desarrolló el cálculo spi en 1997, y con Needham redactó la lista de prácticas prudentes para el diseño de protocolos que todavía detecta errores que los métodos formales pasan por alto.
En 2005, junto con colegas de Microsoft Research, presentó la control-flow integrity, hoy integrada en compiladores y procesadores. En Google fue coautor de TensorFlow y del método de aprendizaje profundo con privacidad diferencial de 2016. Pocos han cambiado tanto de campo sin abandonar nunca la pregunta de qué garantiza realmente un sistema.