Pourquoi IOG a choisi Haskell pour construire Cardano ?

L’équipe d’IOG a soigneusement choisi le langage de programmation et les outils à utiliser pour le développement de Cardano. Au final, elle a choisi Haskell. L’équipe doit être en mesure de vérifier formellement que tout ce qui est écrit dans les livres blancs correspondra correctement au code source. Venez lire comment l’équipe transforme les preuves mathématiques des livres blancs en code source Haskell.

Résumé

• Avant Cardano, aucun projet du top 10 n’utilisait de méthodes formelles.
• Le livre blanc est la base de la spécification formelle. Il est la base du code source écrit en Haskell.
• La spécification formelle et le code source Haskell ont des notations très similaires.

Du livre blanc au code source

De nombreuses équipes dans l’industrie de la blockchain ont une mentalité de startup « move fast and break things ». Cette mentalité est motivée par la jeunesse, la cupidité et la passion. Le code source de nombreux protocoles est souvent écrit à la hâte et sans recherche préalable. Dans certains cas, on peut parler d’une approche irresponsable des équipes vis-à-vis des utilisateurs. L’antithèse est une approche lente, méthodique et académique motivée par le désir de consolider l’innovation dans notre espace. Au moment où l’équipe a commencé à développer Cardano, aucune des dix premières crypto-monnaies en termes de capitalisation boursière n’était basée sur un protocole évalué par les pairs et n’était mise en œuvre sur la base d’une spécification formelle. L’équipe d’IOG a décidé d’utiliser des méthodes formelles pour développer Cardano.

IOG définit et prouve mathématiquement l’exactitude du comportement du protocole et d’autres composants dans des livres blancs. Ces documents sont ensuite utilisés pour créer une spécification formelle. La spécification formelle est une description précise et mathématique du comportement et des propriétés du système.

Dans les livres blancs, la notation mathématique est utilisée pour exprimer des concepts abstraits et des preuves mathématiques. Elle est précise mais peut être difficile à comprendre pour les non-experts. La notation de spécification formelle est utilisée pour exprimer le comportement et les propriétés d’un système logiciel d’une manière précise et mathématique. Elle est moins abstraite que la notation mathématique mais plus précise que le code source. En d’autres termes, le programmeur peut ne pas comprendre la notation mathématique utilisée dans les livres blancs, mais il est capable de comprendre la spécification formelle.

Une fois la spécification formelle créée, l’étape suivante est la mise en œuvre du code source dans le langage de programmation Haskell. Il est attendu que l’implémentation suive les spécifications et les propriétés décrites dans la spécification formelle. L’implémentation doit être réalisée de manière à ce qu’il soit possible de prouver mathématiquement que l’implémentation répond aux exigences et aux propriétés décrites dans la spécification formelle. En d’autres termes, le code source peut être vérifié formellement sur la base de la spécification.

Bien qu’il existe une relation entre la notation mathématique, la notation de spécification formelle et le code source Haskell, il n’est pas toujours facile de passer de l’une à l’autre. Le niveau d’abstraction et d’expressivité de chacun est différent puisque des notations différentes sont utilisées. L’objectif est de maximiser le transfert d’informations entre les différentes notations.

Les scientifiques et les mathématiciens ne sont pas forcément des programmeurs Haskell. Leur travail consiste à rédiger un livre blanc. Les programmeurs Haskell n’ont pas besoin d’être des mathématiciens de haut niveau. La spécification formelle est une sorte de médiateur entre les deux groupes. Il doit y avoir quelqu’un qui est capable de créer une spécification formelle à partir d’un livre blanc. Cependant, il est possible d’utiliser des outils capables de traduire automatiquement entre la notation mathématique, la notation de spécification formelle et le code source, comme les langages de programmation typés de manière dépendante tels que Coq ou Agda.

Cog et Agda sont tous deux des outils de vérification formelle qui peuvent être utilisés dans le contexte de langages de programmation fonctionnelle comme Haskell. Ce sont tous deux des assistants de preuve, c’est-à-dire des programmes informatiques qui aident les utilisateurs à écrire des preuves mathématiques formelles.

Cog et Agda sont tous deux basés sur l’idée d’utiliser des méthodes formelles pour améliorer la fiabilité et la correction des systèmes logiciels. Alors que Cog est plus spécifique aux algorithmes concurrents, Agda est plus général et peut être utilisé pour tout type de programmation fonctionnelle. Ce sont tous deux des outils puissants pour garantir la correction des systèmes logiciels et ils peuvent être utilisés ensemble pour fournir une solution de vérification complète.

Pourquoi Haskell

Haskell est un langage de programmation fonctionnel qui se prête bien à l’utilisation de méthodes formelles pendant le développement de logiciels.

L’un des principaux avantages de Haskell est son solide système de types. Haskell possède un système de types statique, ce qui signifie que les types sont vérifiés au moment de la compilation, offrant ainsi un haut niveau de sécurité et empêchant de nombreux types de bogues avant même l’exécution du programme. En outre, Haskell prend en charge l’inférence de type, ce qui signifie que le programmeur n’a pas besoin de spécifier explicitement les types des variables et des fonctions, ce qui rend le code plus concis et plus lisible.

En Haskell, les variables sont immuables par défaut, ce qui signifie qu’une fois qu’une valeur est attribuée à une variable, elle ne peut plus être modifiée. Cela facilite le raisonnement sur le comportement du programme et peut simplifier la programmation concurrente et parallèle. L’immuabilité permet également d’éviter les bogues causés par des modifications inattendues des variables, et de rendre le code plus testable.

Haskell met également l’accent sur la programmation fonctionnelle, qui encourage un style de programmation déclaratif et expressif. Dans la programmation fonctionnelle, l’accent est mis sur la description de ce que le programme doit faire, plutôt que sur la manière dont il doit le faire. Cela rend le code plus lisible, plus facile à maintenir et peut simplifier le débogage et les tests.

Le solide système de types de Haskell et son style de programmation mathématique en font un outil naturel pour les méthodes formelles. Le système de types de Haskell est très expressif et permet un haut niveau de vérification statique du code. Cela signifie que de nombreuses erreurs de programmation courantes peuvent être détectées au moment de la compilation, plutôt qu’au moment de l’exécution. En outre, le paradigme de la programmation fonctionnelle encourage un style de pensée mathématique, ce qui contribue à rendre le code plus prévisible et plus facile à raisonner. Cela peut être particulièrement bénéfique pour les bases de code Cardano complexes et volumineuses.

Le garbage collection et l’évaluation stricte de Haskell garantissent que le programme est protégé contre les erreurs d’exécution telles que les déréférences de pointeur nul, les débordements de tampon et les courses de données. Cela le rend plus adapté aux systèmes critiques en matière de sécurité.

Le modèle de concurrence et de parallélisme de Haskell, basé sur des threads légers et le passage de messages, permet d’écrire facilement du code qui peut tirer parti de plusieurs cœurs et processeurs. C’est important pour le projet Cardano, qui est une plateforme blockchain devant traiter un grand nombre de transactions simultanément.

Les abstractions de haut niveau de Haskell, telles que les monades, facilitent l’écriture de code modulaire, composable et réutilisable. Cela peut aider à réduire la complexité de la base de code et à faciliter le raisonnement et la preuve des propriétés du code.

Fonction factorielle

Prenons un exemple simple de la façon dont une notation mathématique peut être transformée en code source.

Une preuve mathématique complète de la fonction factorielle ressemblerait à ceci :

Regardez la spécification formelle en Agda de la fonction factorielle :

Regardez la notation Coq de la fonction factorielle :

Voir comment le code source Haskell de la fonction factorielle ressemble à la notation Agda et Coq :

À titre de comparaison, voyez à quoi ressemble l’implémentation de la fonction factorielle dans le langage traditionnel C++ :

Le programmeur doit comprendre la spécification formelle pour être capable d’écrire le code source correspondant en Haskell. Bien entendu, un programmeur peut également écrire une fonction factorielle en C++, mais remarquez que la notation est moins proche de la spécification formelle. Dans les deux cas, le code fait exactement ce que la spécification indique qu’il doit faire, ce qui est la chose la plus importante de toutes.

Cependant, il est plus naturel pour un programmeur de comparer la notation Haskell et les spécifications formelles que s’il devait faire de même avec le C++ (ou un autre langage similaire). La différence serait plus perceptible pour les fonctions plus complexes.

Conclusion

L’équipe d’IOG avait de nombreuses raisons de choisir Haskell. Ce n’est pas seulement le langage lui-même qui est important, mais aussi son adéquation à la résolution d’un problème spécifique, le nombre d’outils disponibles et le nombre de développeurs de qualité. Il n’est pas très courant pour un programmeur ordinaire d’avoir une expérience des méthodes formelles. Dans le cas des programmeurs Haskell, la fréquence est plus élevée. De plus, il est rare de trouver des développeurs Haskell expérimentés sans connaissance approfondie de l’informatique.

Dans le contexte de la nécessité d’utiliser des méthodes formelles pour le développement de Cardano, Haskell était l’un des choix naturels. Cardano est construit comme un projet critique, et Haskell a dans son ADN des caractéristiques qui aident à atteindre cet objectif.

Cet article est une traduction : https://cexplorer.io/article/why-did-iog-choose-haskell-to-build-cardano