Réinventer la programmation ? | InternetActu
▻http://internetactu.blog.lemonde.fr/2017/11/25/reinventer-la-programmation
Les programmeurs doivent s’améliorer
Il n’empêche que bien des logiciels restent fabriqués à l’ancienne. Les ingénieurs écrivent leurs exigences en prose et les programmeurs les codent. Il faut dire que les programmeurs aiment écrire du code. Les outils qui écrivent du code et vérifient son exactitude semblent encore ésotériques à beaucoup, pour ne pas dire trop beaux pour être vrais. Tant et si bien, souligne Somers, qu’il faudrait surtout étudier pourquoi les développeurs sont encore si réfractaires à ces nouvelles méthodes.
En 2011, Chris Newcombe est déjà chez Amazon depuis 7 ans. Ingénieur principal, il a travaillé sur certains des systèmes parmi les plus critiques de l’entreprise, comme le catalogue des produits, l’infrastructure de gestion des Kindle ou encore Amazon Web Services, l’infrastructure de traitement et de stockage à la demande… La complexité des systèmes rend les événements censés être extrêmement rare peut-être plus probable qu’on ne le pense. Pour lui, les algorithmes des systèmes critiques sont souvent parfaits, mais les bugs se révèlent plus difficiles à trouver quand les algorithmes deviennent plus complexes. Et la démultiplication des tests ne suffit pas toujours à les repérer. D’où son excitation quand il a entendu parler de TLA+, un mélange de code et de mathématique pour écrire des algorithmes « parfaits ».
TLA+, qui signifie « Logique temporelle des actions », est similaire en esprit à la conception basée sur le modèle : c’est un langage pour écrire les exigences – TLA+ les appelle « spécifications » – des programmes d’ordinateur. C’est lui aussi un système de méthode formelle. Ces spécifications peuvent ensuite être entièrement vérifiées par un ordinateur. C’est-à-dire, avant d’écrire un code, vous écrivez un bref aperçu de la logique de votre programme, avec les contraintes dont vous avez besoin pour y répondre (par exemple, si vous programmez un guichet automatique, une contrainte pourrait être que vous ne pouvez jamais retirer le même argent deux fois d’un compte chèque). TLA+ vérifie alors de manière exhaustive que votre logique réponde bien à ces contraintes. Sinon, il vous montrera exactement comment ils pourraient être détournés.
