Une très chouette lecture. Une des choses que je retiens, c'est la description du théorème des quatre couleurs et la réception par la communauté en mathématique de sa résolution. Pour le contexte, c'est un théorème qui était resté irrésolu pendant presque un siècle depuis son énoncé (1879, Arthur Cayley). En particulier, la relative tiédeur des mathématicien·nne·s m'a étonné. En cause: la notion de "preuve", perçue tantôt comme un processus d'énoncé, discussion, raffinement et intégration (éminemment social, et pas si éloigné que ça de ce qui se fait dans d'autres disciplines scientifiques), tantôt comme le résultat d'une suite de déduction partant d'axiomes - avec des nuances entre ces deux visions. N'étant pas mathématicien moi-même, je voyais naïvement la "preuve" d'un théorème comme relevant du second procédé, oubliant un peu vite le premier.

Un autre élément que je retiens, c'est l'importance de la NSA et de l'armée dans le financement et le soutien de la recherche en méthodes formelles et en sécurité logicielle. Le livre a un point de vue centré États-Unis (en particulier j'adorerais avoir le même genre d'analyse sur le contexte Français ou Européen), mais les liens entre complexe militaro-industriel et vérification logicielle sont très visiblement mis en lumière.