Fundación Linux lanza Fundación TLA+ con AWS, Oracle y Microsoft para promover lenguaje de programación TLA+

La Fundación Linux, el consorcio tecnológico sin fines de lucro que gestiona varios esfuerzos de código abierto, anunció hoy el lanzamiento de la Fundación TLA+ para promover la adopción y el desarrollo del lenguaje de programación TLA+. AWS, Oracle y Microsoft se encuentran entre los miembros fundadores.

¿Qué es el lenguaje de programación TLA+, te preguntas? Es un lenguaje formal de "especificación" desarrollado por el científico informático y matemático Leslie Lamport. Conocido por su trabajo seminal en sistemas distribuidos, Lamport, ahora científico en Microsoft Research, creó TLA+ para diseñar, modelar, documentar y verificar programas de software, especialmente aquellos de naturaleza concurrente y distribuida.

Para dar algunos ejemplos, ElasticSearch, la organización detrás del motor de búsqueda del mismo nombre, utilizó TLA+ para verificar la corrección de sus algoritmos de sistemas distribuidos. En otro lugar, Thales, la empresa de fabricación de sistemas eléctricos, utilizó TLA+ para modelar y desarrollar módulos tolerantes a fallos para su plataforma de control industrial.

"TLA+ es único en que está destinado a especificar un sistema, en lugar de implementar software", dijo un portavoz de la Fundación Linux por correo electrónico. "Basado en conceptos matemáticos, especialmente en teoría de conjuntos y lógica temporal, TLA+ permite la expresión de las propiedades de corrección deseadas de un sistema de manera formal y rigurosa".

TLA+ incluye un verificador de modelos y un demostrador de teoremas para verificar si la especificación de un sistema satisface sus propiedades deseadas. El objetivo es ayudar a los desarrolladores a razonar sobre los sistemas por encima del nivel de código, descubriendo y previniendo fallos de diseño (con suerte) antes de que evolucionen en errores durante las etapas posteriores de la ingeniería de software.

En ese último punto, las fallas en el diseño de software son sorprendentemente comunes y disruptivas. Un informe de 2020 del Grupo Standish encontró que alrededor del 66% de los proyectos de software fallan. Y según el Consorcio de Calidad de la Información y el Software, la mala calidad del software costó a las empresas más de $2 billones en 2020.

Con el establecimiento de la Fundación TLA+, la Fundación Linux dice que proporcionará recursos de educación y capacitación en torno a TLA+, financiará la investigación y desarrollará herramientas para ella y trabajará para fomentar una comunidad de practicantes de TLA+. La Fundación TLA+ también tomará decisiones sobre mejoras en el lenguaje, abordará los comentarios de los usuarios y guiará la evolución del lenguaje.

"TLA+ ya ha sido utilizado con éxito por importantes empresas de tecnología como Amazon, Oracle y Microsoft para verificar y diseñar sistemas a escala planetaria", continuó el portavoz. "Al establecer una Fundación TLA+ bajo el paraguas de la Fundación Linux, TLA+ ganará mayor visibilidad y apoyo, promoviendo su adopción más amplia dentro de la industria tecnológica. La misión de la fundación de abogar por proyectos de código abierto garantizará que TLA+ continúe evolucionando y siga siendo accesible para la comunidad tecnológica en general. Además, la fundación facilitará una mayor colaboración entre la industria y la academia, avanzando en el estado del arte en métodos formales y en la investigación de sistemas concurrentes y distribuidos".