Le Linux Fondationle consortium technologique à but non lucratif qui gère divers efforts open source, a annoncé aujourd’hui le lancement du TLA+ Fondation promouvoir l’adoption et le développement du langage de programmation TLA+. AWS, Oracle et Microsoft font partie des premiers membres.
Qu’est-ce que le langage de programmation TLA+, demandez-vous ? C’est un langage formel « spec » développé par l’informaticien et mathématicien Leslie Lamport. Mieux connu pour son travail fondateur sur les systèmes distribués, Lamport – maintenant scientifique chez Microsoft Research – a créé TLA + pour concevoir, modéliser, documenter et vérifier les programmes logiciels – en particulier ceux de la variété concurrente et distribuée.
Pour donner quelques exemples, ElasticSearch, l’organisation à l’origine du moteur de recherche du même nom, a utilisé TLA+ pour vérifier l’exactitude des algorithmes de ses systèmes distribués. Par ailleurs, Thales, l’entreprise de fabrication de systèmes électriques, a utilisé TLA+ pour modéliser et développer des modules tolérants aux pannes pour sa plate-forme de contrôle industriel.
« TLA + est unique en ce sens qu’il est destiné à spécifier un système plutôt qu’à implémenter un logiciel », a déclaré un porte-parole de la Linux Foundation à TechCrunch par e-mail. « Basé sur des concepts mathématiques, notamment la théorie des ensembles et la logique temporelle, TLA+ permet d’exprimer les propriétés d’exactitude souhaitées d’un système de manière formelle et rigoureuse. »
TLA+ comprend un vérificateur de modèle et démonstrateur de théorèmes pour vérifier si la spécification d’un système satisfait ses propriétés souhaitées. L’objectif est d’aider les développeurs à raisonner sur les systèmes au-dessus du niveau du code, en découvrant et en prévenant les défauts de conception (espérons-le) avant qu’ils ne se transforment en bogues au cours des dernières étapes de l’ingénierie logicielle.
Sur ce dernier point, les échecs dans la conception de logiciels sont étonnamment courants et perturbateurs. Un rapport de 2020 du Standish Group a révélé qu’environ 66% des projets logiciels échouent. Et selon le Consortium for Information and Software Quality, la mauvaise qualité des logiciels a coûté aux entreprises plus de 2 000 milliards de dollars en 2020.
Avec la création de la Fondation TLA+, la Fondation Linux annonce qu’elle fournira des ressources d’éducation et de formation autour de TLA+, financera la recherche et développera des outils pour cela et travaillera pour favoriser une communauté de praticiens TLA+. La Fondation TLA+ prendra également des décisions sur les améliorations du langage, répondra aux commentaires des utilisateurs et guidera l’évolution du langage.
« TLA + a déjà été utilisé avec succès par de grandes entreprises technologiques comme Amazon, Oracle et Microsoft pour vérifier et concevoir des systèmes à l’échelle planétaire », a poursuivi le porte-parole. « En créant une fondation TLA+ sous l’égide de la fondation Linux, TLA+ gagnera en visibilité et en soutien, favorisant son adoption plus large au sein de l’industrie technologique. La mission de la fondation de défendre les projets open source garantira que TLA + continue d’évoluer et reste accessible à la communauté technologique au sens large. De plus, la fondation facilitera une plus grande collaboration entre l’industrie et le milieu universitaire, faisant progresser l’état de l’art dans les méthodes formelles et la recherche sur les systèmes simultanés et distribués.