Software, between mind and matter

A computer can perform many different functions just by changing the piece of software it executes. This amazing plasticity of software enabled the digital computer to escape data centers and spread everywhere, from everyday objects to critical infrastructures. Which fundamental concepts underlie this technical feat? How can we master the amazing and often frightening complexity of software? How can we avoid programming bugs and resist security attacks? How can we establish that a piece of software is safe and trustworthy? To these questions, mathematical logic offers answers that enable us to build a scientifically rigorous approach to software. (This is an English translation of Xavier Leroy's inaugural lecture at College de France.)