La fondation Linux a annoncé vendredi 21 avril 2023 la création de la TLA+ Foundation afin de promouvoir l'adoption du langage de programmation du même nom et le développement d'une communauté afférente d’utilisateurs. TLA+ (acronyme de Temporal Logic of Actions) est un langage formel de spécification de haut niveau conçu pour la modélisation et la vérification d’algorithmes et de systèmes parallèles et distribués.
Selon l’organisme, TLA+ a été utilisé avec succès par des entreprises pour vérifier des systèmes logiciels complexes, réduire les erreurs et améliorer la fiabilité. Le langage aide notamment à détecter les erreurs de conception au début du processus de développement, en particulier celles qui sont difficiles à débusquer et coûteuses à corriger dans un code. TLA+ s’appuie à cet égard sur l'idée que la meilleure façon de décrire les choses avec précision est d’utiliser des fonctions mathématiques simples.
« Nvidia utilise des méthodes formelles pour le développement de logiciels et matériels critiques au niveau de la sûreté et de la sécurité, y compris TLA+, que nous utilisons pour formaliser nos conceptions et nos exigences, indique Tom McReynolds, directeur en charge de la plate-forme logicielle automobile Drive OS pour la société américaine. La création de la TLA+ Foundation comble une lacune importante en fournissant une plate-forme gérée par des professionnels et en permettant le partage de contributions, d’expériences et des meilleures pratiques. Cela ne pourra qu’améliorer le langage TLA+, renforcer la vérification de modèles et rendre les outils plus faciles à utiliser. La TLA+ Foundation répond à un autre besoin important qu’est la promotion de l'utilisation plus large de méthodes formelles dans l'industrie pour améliorer la qualité des produits, en particulier là où la sûreté et la sécurité sont essentielles. »
TLA+ a été inventé il y a plusieurs décennies par le chercheur en informatique Leslie Lamport, aujourd'hui éminent scientifique de Microsoft Research. Après des années de gérance de Lamport et de soutien de Microsoft, le langage sera donc désormais pris en charge par la TLA+ Foundation qui compte parmi ses premiers membres Amazon Web Services (AWS), Oracle et Microsoft.
Cette structure compte encourager l'adoption du langage en maintenant des critères élevés de fiabilité et de sûreté, fournir des ressources d'éducation et de formation, financer la recherche, développer des outils et créer une communauté d’utilisateurs. Parmi les entreprises et laboratoires de recherche à apporter leur soutien à l’initiative de la fondation Linux figurent aussi Google, Informal Systems (une société créée en 2020 et spécialiste des protocoles de blockchain), l’Inria, Nvidia et Oracle.
