La Fundación Linux, el consorcio tecnológico sin fines de lucro que administra 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 inaugurales.
¿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. Mejor conocido por su trabajo seminal en sistemas distribuidos, Lamport, ahora científico de Microsoft Research, creó TLA+ para diseñar, modelar, documentar y verificar programas de software, particularmente aquellos de la variedad concurrente y distribuida.
Para dar algunos ejemplos, ElasticSearch, la organización detrás del motor de búsqueda del mismo nombre, usó TLA+ para verificar la corrección de sus algoritmos de sistemas distribuidos. Por otra parte, Thales, la empresa de fabricación de sistemas eléctricos, utilizó 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á destinado a especificar un sistema, en lugar de 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 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 probador de teoremas para verificar si la especificación de un sistema satisface las propiedades deseadas. El objetivo es ayudar a los desarrolladores a razonar sobre sistemas por encima del nivel de código, descubriendo y previniendo fallas de diseño (con suerte) antes de que se conviertan en errores durante las últimas etapas de la ingeniería de software.
Hasta ese último punto, las fallas en el diseño de software son sorprendentemente comunes y disruptivas. Un 2020 informe del Standish Group encontró que alrededor del 66% de los proyectos de software fallan. Y de acuerdo a Según el Consorcio para la Calidad de la Información y el Software, la mala calidad del software le costó a las empresas más de 2 billones de dólares 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 ello y trabajará para fomentar una comunidad de practicantes de TLA+. La Fundación TLA+ también tomará decisiones sobre las mejoras del idioma, abordará los comentarios de los usuarios y guiará la evolución del idioma.
“TLA+ ya ha sido utilizado con éxito por importantes empresas tecnológicas 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+ obtendrá una 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 permanezca accesible para la comunidad tecnológica en general. Además, la fundación facilitará una mayor colaboración entre la industria y la academia, impulsando el estado del arte en métodos formales e investigación de sistemas concurrentes y distribuidos”.
Source link