Martín Abadi
Informaticien argentin qui a fait des protocoles de sécurité un objet sur lequel on peut démontrer des choses, avant d'appliquer la même rigueur à l'apprentissage automatique.
La logique BAN (1989, avec Michael Burrows et Roger Needham) est le premier outil formel pratique pour raisonner sur ce que les participants à un protocole d'authentification sont en droit de croire. Avec Andrew Gordon, il développe le calcul spi en 1997 ; avec Needham, il rédige la liste de bonnes pratiques d'ingénierie pour concevoir des protocoles, qui attrape encore des bogues que les méthodes formelles laissent passer.
En 2005, avec des collègues de Microsoft Research, il introduit l'intégrité du flot de contrôle, aujourd'hui intégrée aux compilateurs et aux processeurs. Chez Google, il co-signe TensorFlow et, en 2016, la méthode d'apprentissage profond différentiellement privé. Peu de gens ont changé de domaine aussi souvent sans jamais quitter la question de ce qu'un système garantit réellement.