The Linux Foundation, la organización sin fines de lucro que permite la innovación masiva a través del código abierto, anunció hoy el lanzamiento de TLA+ Foundation para promover la adopción y el desarrollo del lenguaje de programación TLA+ y su comunidad de practicantes de TLA+. Los miembros inaugurales incluyen Amazon Web Services (AWS), Oracle y Microsoft. TLA+ es un lenguaje de alto nivel para modelar programas y sistemas, especialmente simultáneos y distribuidos. Las empresas han utilizado con éxito TLA+ para verificar sistemas de software complejos, reduciendo errores y mejorando la confiabilidad. El lenguaje ayuda a detectar fallas de diseño en una etapa temprana del proceso de desarrollo, lo que ahorra tiempo y recursos.
TLA+ y sus herramientas son útiles para eliminar errores de diseño fundamentales, que son difíciles de encontrar y costosos de corregir en el código. El lenguaje se basa en la idea de que la mejor manera de describir las cosas con precisión es con matemáticas simples. El lenguaje fue inventado hace décadas por el científico informático pionero Leslie Lamport, ahora un científico distinguido de Microsoft Research. Después de años de administración de Lamport y el apoyo de Microsoft, TLA+ ha encontrado un nuevo hogar en la Fundación Linux.
«El establecimiento de la Fundación TLA+ demuestra el compromiso de promover el uso y desarrollo del lenguaje TLA+ en beneficio de toda la industria del software», dijo Jim Zemlin, director ejecutivo de la Fundación Linux. «A medida que crece la dependencia mundial de los sistemas distribuidos, es importante que los desarrolladores cuenten con las capacidades de TLA+ para modelar y verificar formalmente que los sistemas se comporten como se esperaba».
La Fundación TLA+ promoverá la adopción, proporcionará recursos de educación y capacitación, financiará la investigación, desarrollará herramientas y construirá una comunidad de profesionales de TLA+. El papel de la Fundación TLA+ como comité lingüístico garantizará la mejora y evolución continuas del lenguaje TLA+. La Fundación TLA+ tomará decisiones sobre las mejoras del idioma, abordará los comentarios y las necesidades de los usuarios, mantendrá altos estándares de seguridad y confiabilidad y guiará la evolución del idioma para servir mejor a su base de usuarios.
«AWS se compromete a brindar servicios de alta calidad a nuestros clientes, razón por la cual nuestro equipo de razonamiento automatizado se ha basado en técnicas como la especificación formal y la verificación de modelos durante años para resolver problemas de diseño difíciles en sistemas críticos. TLA+ es una herramienta poderosa en nuestra caja de herramientas eso nos ayuda a verificar la corrección de nuestros sistemas de software bajo suposiciones. Al unirnos a la Fundación TLA+, nuestro objetivo es apoyar el avance de las herramientas TLA+ y mejorar aún más el estado del arte en el diseño de sistemas distribuidos «, dijo Byron Cook, vicepresidente y Científico Distinguido en AWS.
«En Microsoft, un número cada vez mayor de equipos de ingeniería han confiado en TLA+ para especificar y validar la corrección de sus algoritmos y sistemas de software. Los equipos de ingeniería que utilizan TLA+ han reportado un gran valor al definir con precisión los sistemas y validarlos antes en el ciclo de vida de la ingeniería. Las herramientas de TLA+ han ayudado a identificar problemas con sus diseños antes de escribir una sola línea de código. Al unirnos a la Fundación TLA+, nuestro objetivo es fomentar una comunidad de profesionales de TLA+ que se preocupan profundamente por diseñar sistemas distribuidos correctos». dijo Dharma Shukla, miembro técnico de Microsoft.
«Los servicios en la nube distribuidos a gran escala forman la columna vertebral de todas las plataformas en la nube hiperescaladoras, incluida Oracle Cloud Infrastructure (OCI). Cuando lanzamos en 2016, OCI fue la primera nube diseñada utilizando métodos formales desde el principio para brindar servicios en la nube de alta calidad. En OCI , usamos TLA+ en más de 25 de nuestros servicios más críticos, incluidos los servicios de almacenamiento de archivos y almacenamiento en bloque, para verificar la corrección de escenarios de diseño complejos, incluida la replicación distribuida, la conmutación por error y la fragmentación en vivo. miembro fundador con el objetivo de promover el conjunto de herramientas TLA+ y mejorar la calidad de los servicios distribuidos en la nube en los años venideros». dijo Pradeep Vincent, vicepresidente sénior y arquitecto técnico jefe de OCI, Oracle.
«La Fundación TLA+ es oportuna de muchas maneras. Ahora más que nunca es necesario pensar de manera sistémica y analítica sobre el desarrollo de software. La complejidad de los sistemas de software de redes frecuentes está aumentando y necesitamos herramientas como TLA+ para hacer frente». dijo Vint Cerf, vicepresidente y evangelista jefe de Internet en Google.
«Desde su inicio en 2020, Informal Systems ha estado utilizando TLA+ para especificar protocolos de cadena de bloques como Tendermint Consensus, el protocolo de cliente ligero y el Protocolo de comunicación entre cadenas de bloques (IBC). En combinación con el verificador de modelos Apalache, estas especificaciones reforzaron la confianza de la comunidad de Cosmos en estos protocolos. La flexibilidad de TLA+ también nos permite iniciar el programa de auditorías de seguridad en un corto período de tiempo. Aplicamos Apalache para encontrar problemas de seguridad en aplicaciones distribuidas impulsadas por la tecnología Cosmos». dijo Igor Konnov, científico investigador principal de Informal Systems.
“Inria está comprometida con el fomento de la investigación al más alto nivel internacional así como con la transferencia de los resultados de esa investigación para que tengan un impacto en la industria y la sociedad. Los investigadores de Inria han contribuido a la evolución del lenguaje TLA+ y al diseño de verificación herramientas para TLA+. La creación de la Fundación TLA+ ayuda a garantizar que el mayor desarrollo del lenguaje y sus herramientas sea un esfuerzo conjunto de la comunidad académica e industrial en general interesada en el diseño de sistemas distribuidos confiables». dijo Stephan Merz, investigador sénior de Inria y jefe del equipo del proyecto VeriDis.
«NVIDIA usa activamente métodos formales en el desarrollo de software y hardware críticos para la seguridad y la protección, incluido TLA+, que usamos para formalizar nuestros diseños y requisitos. Vemos que la Fundación TLA+ llena un vacío importante al proporcionar una plataforma administrada profesionalmente para compartir contribuciones, Experiencias y mejores prácticas. Puede convertirse en una fuerza impulsora para mejorar aún más el producto TLA+: mejorar el lenguaje TLA+, hacer que la verificación de modelos sea más poderosa y hacer que las herramientas sean más fáciles de usar. Se necesita una colaboración independiente y abierta dentro de la fundación para asegurar el futuro de TLA+ como un ecosistema popular y activamente desarrollado. La fundación TLA+ satisface otra necesidad importante: promover el uso más amplio de métodos formales en la industria para mejorar la calidad del producto, especialmente donde la seguridad y la protección son críticas». dijo Tom McReynolds,
La Fundación TLA+ invita a las empresas de tecnología a unirse y apoyar su misión de promover el desarrollo de TLA+ en la industria del software. Al trabajar juntos, la Fundación TLA+ puede continuar mejorando las capacidades de este importante lenguaje y ayudar a garantizar que los beneficios de TLA+ estén disponibles para todos. Para obtener más información sobre la Fundación TLA+, visite foundation.tlapl.us
