La Fondation TLA+ vise à généraliser la modélisation logicielle basée sur les mathématiques – Microsoft Research

TLA + est un langage mathématique de haut niveau, open source, pour la modélisation de programmes et de systèmes informatiques, en particulier les systèmes concurrents et distribués. Il est livré avec des outils pour aider à éliminer les erreurs de conception fondamentales, qui sont difficiles à trouver et coûteuses à corriger une fois qu’elles ont été intégrées dans le code ou le matériel.

Le langage TLA a été publié pour la première fois en 1993 par l’informaticien pionnier Leslie Lamport, aujourd’hui éminent scientifique de Microsoft Research. Après des années de gérance de Lamport et de soutien de Microsoft, TLA+ a trouvé un nouveau foyer. La Fondation TLA + est lancée ce mois-ci dans le cadre de la Linux Foundation, avec Microsoft, Amazon Web Services (AWS) et Oracle en tant que membres fondateurs pour aider à affiner davantage les outils et stimuler l’utilisation commerciale et la recherche supplémentaire.

La fondation aidera à diffuser ce travail entre plusieurs mains, a déclaré Lamport.

TLA+ n’est qu’un élément du portefeuille impressionnant de Lamport. Il a inventé le système de préparation de documents LaTeX et a remporté le prix Turing 2013 pour son travail de clarification des systèmes distribués, dans lesquels plusieurs ordinateurs autonomes communiquent entre eux en passant des messages.

En cours de route, il a développé une idée pour aider les programmeurs à construire des systèmes plus efficacement en utilisant des modèles algorithmiques pour spécifier le fonctionnement du code. C’est la même idée que de créer des plans pour guider la construction d’un pont. TLA + (pour Temporal Logic of Actions) est livré avec un vérificateur de modèle qui vérifiera si la satisfaction d’une spécification de programme implique que le code fera ce qu’il doit faire.

Lorsque les programmeurs écrivent des systèmes, ils doivent commencer par définir ce qu’ils sont censés faire et vérifier que leur travail le fera. C’est une meilleure façon que de simplement s’asseoir pour écrire le code, basé sur un vague aperçu, a déclaré Lamport.

Pour les tâches simples, une approche par essais et erreurs peut convenir. Mais pour les projets plus compliqués, ou ceux où les erreurs sont inacceptables, une approche systématique a plus de sens.

Le défi avec l’écriture de grands programmes n’est pas nécessairement leur taille, c’est leur complexité. Ils sont souvent répartis sur plusieurs systèmes et impliquent plusieurs processus qui doivent interagir. Le nombre d’exécutions possibles devient astronomique. Pour raisonner et vérifier un tel système, il est utile d’avoir une manière mathématique d’y penser en amont. Pourtant, les ingénieurs rechignent souvent à l’idée.

La difficulté qu’ont les ingénieurs est plus une peur des maths que les maths elles-mêmes. Les mathématiques, en tant que mathématiques, sont très basiques, a déclaré Lamport, même s’il convient de noter qu’il est titulaire d’un doctorat en mathématiques. Je trouve que les ingénieurs, après avoir utilisé TLA+, comprennent l’avantage.

En fait, TLA + a été adopté pour une utilisation industrielle chez les fabricants de semi-conducteurs, les entreprises qui construisent des systèmes distribués et de bases de données, d’autres entreprises technologiques et dans des applications plus courantes comme les systèmes de paiement dans les magasins de détail. Il est probable que certaines applications ne soient pas rendues publiques, la plupart des entreprises ne discutent pas publiquement de leur processus d’ingénierie ou de leur technologie propriétaire.

C’est là que la fondation entre en jeu. Un système formel pour contribuer aux outils et définir leur orientation future peut engendrer une collaboration supplémentaire entre les ingénieurs et faciliter l’adoption commerciale. La fondation créera un comité de pilotage, similaire à d’autres panels qui s’occupent des langages de programmation du domaine public comme C ou Java.

J’espère que les nouveaux stewards feront plus de soustractions que d’ajouts au langage, pour supprimer certaines choses qui ne sont pas nécessaires, a déclaré Lamport.

Aujourd’hui âgé de 82 ans et proche de la retraite, Lamport espère également que la fondation rapprochera TLA+ du courant dominant des discussions industrielles et universitaires.

TLA+ ne sera jamais aussi populaire que Java. Et je serais heureux si quelqu’un d’autre faisait mieux pour aider les ingénieurs à penser plus mathématiquement, dit Lamport. Le but ultime est d’amener les ingénieurs à réfléchir rigoureusement à un niveau supérieur sur ce qu’ils font.