Martín Abadi
Argentine computer scientist who turned security protocols into something you could prove things about, then brought the same rigour to machine learning.
BAN logic (1989, with Michael Burrows and Roger Needham) was the first practical formal tool for reasoning about what participants in an authentication protocol are entitled to believe. With Andrew Gordon he developed the spi calculus in 1997, and with Needham he wrote the list of prudent engineering practices for protocol design that still catches bugs formal methods miss.
In 2005 he and colleagues at Microsoft Research introduced control-flow integrity, now built into compilers and CPUs. At Google he co-authored TensorFlow and the 2016 method for differentially private deep learning. Few people have changed fields this often without ever leaving the question of what a system actually guarantees.