🇫🇷 Construire Cardano : fusion des méthodes formelles et du développement agile

[Psychomb]

Auteur : Philipp Kant, directeur des méthodes formelles chez I.O.H.K., présente notre méthodologie pour construire des logiciels avec souplesse et précision

Traduction : The Stakhanovite Stake Pool - STKH

Forme et fonction

I.O.H.K. est en train de faire de Cardano un système d’exploitation pour le monde financier et social à l’échelle globale. Cette tâche énorme exige à la fois une itération rapide et une précision absolue. C’est pourquoi I.O.H.K. a choisi de combiner la rapidité du développement agile du code avec des méthodes formelles de haute assurance. Cette fusion a conduit nos ingénieurs à être les pionniers de cette philosophie de développement moderne.

I.O.H.K. croit fermement à la recherche, aux méthodes formelles, à la programmation fonctionnelle et à la construction rigoureuse. En tant que concurrent dans l’industrie du développement de la blockchain, nous devons également faire preuve de progrès constants et créer de la valeur pour notre communauté mondiale. Cela signifie que nous ne pouvons pas faire de compromis sur la robustesse ou sur la vitesse et la flexibilité du développement. Dans un marché en constante évolution, c’est un défi, et nos développeurs doivent donc trouver le bon équilibre.

Méthode agile contre méthode formelle

Jusque là, la norme pour développer une technologie a été de construire rapidement un produit minimal et viable, puis d’itérer continuellement jusqu’à ce qu’il soit prêt pour le marché de masse. C’est ce qu’on appelle un processus agile. C’est un excellent moyen de montrer qu’un projet progresse tout en construisant au final un produit pleinement fonctionnel. Cependant, une méthodologie agile suppose qu’il y aura des ‘bugs’ et des faiblesses à chaque étape du développement qui pourront être éliminés plus tard. C’est très bien si personne ne risque rien - mais, avec les monnaies virtuelles, il y a une énorme somme d’argent et la confiance des parties prenantes en jeu.

La construction d’un actif numérique sur une blockchain présente plusieurs défis à surmonter pour ce qui est de l’organisation du processus de développement. En tant que cryptomonnaie basée sur la preuve d’enjeu, Cardano est un système distribué qui évolue dans un environnement rempli d’adversaires et où les performances sont essentielle. Le protocole doit maintenir la sécurité face à des acteurs malveillants qui tentent de saboter le système. Cela signifie que personne ne peut se permettre de construire rapidement et de traiter les problèmes plus tard.

La confiance est essentielle pour qu’une monnaie soit acceptée et les preuves d’exactitude sont un bon moyen d’augmenter la véracité d’un système. C’est pourquoi le code ne doit pas seulement être correct, mais il doit y avoir des preuves de son exactitude, comme des tests et des preuves mathématiques. Dans une industrie jeune comme celle des cryptomonnaies, les ingénieurs de I.O.H.K. doivent anticiper l’ajout de nouvelles fonctionnalités tout en maintenant les garanties d’exactitude établies dans les versions initiales. La plateforme ne peut s’étendre à l’échelle mondiale que si elle est capable de se développer tout en maintenant la sécurité et l’utilité pour tous. C’est pourquoi les développeurs de Cardano ont rationalisé leur méthodologie, en combinant une variété d’outils allant des tests basés sur les propriétés jusqu’aux preuves vérifiables par la machine, afin de créer des logiciels de haute assurance même en présence d’exigences changeantes.

La recherche pour coder

La méthodologie commence par la recherche scientifique. À ce jour, l.O.H.K. a publié plus de 60 documents de recherche qui ont contribué à la création de la plate-forme. Chaque document examine un aspect critique de la technologie des blockchain à partir de principes de base. Comment parvenir à un consensus de manière décentralisée ? Comment concevoir un contrat intelligent ? Quelle est la bonne structure de récompense pour encourager un bon comportement ? Les chercheurs d’ l.O.H.K. examinent ces questions et soumettent leurs réponses à des revues scientifiques et à des conférences. Ces articles contiennent des preuves qui doivent être soumises à un examen rigoureux par les pairs. Ensuite, pour s’assurer que la qualité de nos logiciels rend justice à la science, ces derniers sont développés selon des méthodes formelles.

Cela signifie essentiellement que les ingénieurs d’ l.O.H.K. spécifient ce que le code doit faire mathématiquement. De cette façon, ils peuvent s’assurer que lorsque le code est exécuté, il contient les propriétés souhaitées. Le code est écrit en Haskell, un langage de programmation fonctionnel très sûr, avec un système de ‘types’ fort. Bien que Haskell soit un excellent outil pour mettre en œuvre des logiciels fiables, il n’est pas infaillible, de sorte que le code doit encore être testé. Une excellente façon d’écrire des tests est d’utiliser QuickCheck. Cela permet aux développeurs d’indiquer les propriétés qui devraient toujours être présentes dans un programme. QuickCheck génère ensuite des scénarios de test et recherche les contre-exemples minimaux qui violent ces propriétés.

Dans le code qui interagit avec le monde extérieur, en particulier les applications réseau, il peut être difficile de trouver des contre-exemples minimaux. En effet, l’ordre d’exécution n’est pas déterministe : il peut changer à chaque fois que le logiciel est exécuté. Le même code peut être exécuté des centaines de fois, et ne peut échouer qu’une seule fois. Nous pouvons contourner ce problème en utilisant des simulations avec un ordre d’exécution déterministe. L’exécution de tests en simulation nous permet de trouver et de corriger de manière fiable une classe de bugs dans les tests, qui autrement ne se produiraient qu’au hasard en production.

Construire un pont

Pour avoir une idée de la méthodologie de développement employée pour Cardano, considérons la métaphore de la construction de ponts. Lorsqu’un ingénieur civil construit un pont, il passe une grande partie de son temps derrière un bureau. Il planifie une conception, fait ses calculs et commande des relevés géographiques et géologiques. Pendant ce temps, il ne se passe rien sur le chantier. Un observateur ne pourrait pas voir les progrès réalisés. Pour la construction de ponts, c’est la bonne approche. La planification n’est pas précise et il est difficile et coûteux de corriger les problèmes à un stade ultérieur. En fin de compte, le choix se résume en un pont retardé à un coût plus élevé ou alors un pont qui s’effondrerait. L’absence de progrès visibles est un prix raisonnable à payer pour un pont fonctionnel et sûr.

Lors de la fabrication d’un logiciel, il est beaucoup plus facile d’apporter des modifications à un stade ultérieur que lors de la construction d’un pont. C’est ce qui rend l’approche de développement agile commune. Si un développeur agile construisait un pont, il construirait un pilier dans un sprint rapide, puis le suivant dans un second sprint. L’écart entre les piliers serait comblé lors d’un sprint final et, si les choses ne tenaient pas, les développeurs ajouteraient un sprint supplémentaire pour résoudre les problèmes. Si les progrès sont visibles sur le chantier, le produit final risque de présenter de nombreux problèmes. Cela crée un travail de nettoyage à la fin du projet qui aurait pu être évité par une meilleure planification à un stade plus précoce. En outre, le produit viable minimum serait probablement donné à un petit groupe de personnes pour un essai en conditions réelles, en espérant qu’il échoue, afin d’alerter les développeurs sur d’éventuels bugs. Il va sans dire qu’il est préférable que les ponts autoroutiers ne soient pas conçus de cette manière.

En entendant les mots “méthodes formelles”, beaucoup de personnes travaillant dans le développement de logiciels pensent à l’approche du génie civil, qui est surnommée “cascade” et cette dernère est généralement rejetée. Il s’agit d’un malentendu courant mais regrettable. En effet, l’utilisation de techniques formelles appropriées nous permet d’avoir le beurre et l’argent du beurre : avoir une conception globale (une conception délibérée, et non accidentelle par l’assemblage de pièces développées au cours de sprints), montrer des progrès en permanence, et conserver la capacité de réagir à des exigences changeantes.

Une technique clé utilisée par les développeurs d’I.O.H.K. est celle des spécifications exécutables. Ce sont des conceptions de haut niveau, qui font abstraction de détails de bas niveau, écrites dans un langage que l’ordinateur peut comprendre et exécuter. Les spécifications exécutables peuvent être utilisées comme des prototypes pour montrer les progrès réalisés, obtenir les réactions des utilisateurs et tester des hypothèses. De plus, des détails de plus bas niveau peuvent être ajoutés par des raffinements successifs. Nos développeurs construisent d’bord le pont pour résoudre les plus gros problèmes en premier lieu, puis ajoutent des piliers pour le renforcer ultérieurement. Dans un système logiciel, les piliers seraient des fonctionnalités comme la sauvegarde de données sur disque ou l’utilisation d’algorithmes performants, qui sont nécessaires pour un produit final, mais qui ne sont pas essentiels pour démontrer la fonctionnalité globale.

En utilisant des spécifications exécutables, on obtient les avantages d’une planification adéquate sans sacrifier la flexibilité. Les développeurs d’I.O.H.K. peuvent fixer ce à quoi le système devrait ressembler à grande échelle, puis mettre en œuvre les composants appropriés selon les besoins. Des tests continus garantissent que chaque composant s’adapte à la conception globale. Cela permet d’éviter des problèmes qui sont courants dans une approche d’intégration tardive. Avec cette méthodologie, nous obtenons le meilleur des deux mondes : nous pouvons utiliser une conception de haut niveau (en évitant les problèmes d’intégration tardive, en ayant une bonne maîtrise de la conception globale à tout moment), et disposer d’un code qui fonctionne relativement tôt (en démontrant les progrès, et en permettant des tests et des retours d’information tout au long du processus).

À l’épreuve du temps

En fin de compte, la méthode de construction doit être déterminée par ce qui est construit. I.O.H.K. construit un système de fonctionnement social et financier mondial qui exige rigueur et rapidité. Opposer méthodes formelles contre développement agile est une fausse dichotomie. Au lieu de cela, nous continuons à développer notre méthodologie qui fusionne le meilleur des deux approches : des techniques formelles dans un cadre de livraison rapide, avec un code d’assurance solide et plus élevé sur lequel nous pouvons construire pour tous les futurs possibles.