The Linux Foundation, el consorcio de tecnología sin fines de lucro que administra varios proyectos de código abierto, anunció hoy que Lanzamiento de la Fundación TLA+ Promover la adopción y desarrollo del lenguaje de programación TLA+. AWS, Oracle y Microsoft son los primeros miembros. De un informe: ¿Qué es el lenguaje de programación TLA+? Es un lenguaje de «especificación» formal desarrollado por la científica informática y matemática Leslie Lamport. Conocido por su trabajo pionero en sistemas distribuidos, Lamport, ahora científico en Microsoft Research, creó TLA+ para diseñar, modelar, documentar y verificar programas de software, especialmente aquellos que son programas concurrentes y distribuidos.
Por nombrar algunos, ElasticSearch, la organización detrás del motor de búsqueda del mismo nombre, utiliza TLA+ para verificar la corrección de los algoritmos de su sistema distribuido. Por otra parte, la empresa de fabricación de sistemas eléctricos Thales utiliza TLA+ para modelar y desarrollar módulos tolerantes a fallas para su plataforma de control industrial. «TLA+ es único en el sentido de que está diseñado para especificar un sistema, no para implementar software», dijo un portavoz de la Fundación Linux a TechCrunch por correo electrónico. «Basado en conceptos matemáticos, en particular la teoría de conjuntos y la lógica temporal, TLA+ permite expresar las propiedades de corrección requeridas de un sistema de manera formal y rigurosa».
