El internet descubre TLA+, la herramienta de modelado formal de 30 años
The internet discovers TLA+. Now what?
Un tuit de Boris Cherny sobre TLA+ acumuló un millón de vistas y despertó curiosidad masiva por este lenguaje de especificación formal. El artículo explica qué es TLA+, sus límites y cómo la empresa Reasonable construyó un pipeline que convirtió más de 16.000 especificaciones TLA+ en más de 3.000 pruebas Verus verificadas por máquina.
La pregunta interesante, entonces, no es solo si un agente puede escribir TLA+. Es qué se vuelve posible una vez que los agentes pueden moverse entre especificaciones, pruebas y programas reales.
- lopatin
Animaría a todo el mundo a probar esto en problemas autocontenidos, tipo máquinas de estados, si tienen alguno. En mi empresa, algunos expertos estaban optimizando nuestra lógica de clustering y failover añadiendo un poco más de estado (y por tanto complejidad). A pesar de que no soy un experto en esa área, fui capaz de encontrar y prevenir un bug catastrófico apuntando a Opus armado con TLA+ al problema. Era un bug que no era posible en la implementación previa del sistema y a nadie se le ocurrió escribir tests unitarios para la secuencia de pasos que lo desencadena, así que inicialmente pasó desapercibido. Lo único que lo detectó fueron los invariantes de TLA+, que, sí, también los escribió Opus.
Como nota al margen, se habla mucho de que programar ya no es satisfactorio. Pero el ejercicio anterior fue probablemente lo más divertido que he hecho con la ingeniería en mucho tiempo, y habría sido casi imposible para mí personalmente sin IA. Quizás fue la novedad de lo de TLA+, pero creo que ofrece un atisbo de lo que nuestros trabajos podrían ser realmente en el futuro, más allá de simplemente decirle a Claude que haga lo que antes hacías manualmente y luego pulsar enter. Hay casos de uso mucho más ambiciosos y satisfactorios para ello.
- stevefan1999
Uso TLA+ indirectamente a través de https://github.com/quint-co/quint. Añadí instrucciones de que "antes de implementar cualquier característica, por favor usa Quint para modelarla y asegurarte de que no hay contraejemplo para el sistema en su conjunto, reitera el diseño con Quint también y asegúrate de que tus documentos e implementación siguen el modelo formal y la documentación".
El resultado, aunque lleva mucho más tiempo, es bastante mágico. Se encontraron y corrigieron muchos bugs de transacciones y atomicidad solo con tener una instrucción tan simple.
Sin embargo, a veces no todo es mágico, especialmente en lo que respecta a recursos externos. Cloudflare, por desgracia, a veces tiene hipos en D1 y KV con timeouts, lo cual es más o menos fuerza mayor.
Afortunadamente, eso significa que tendré que modelar la acción como un evento binario, que la transacción puede no completarse como habríamos pensado garantizado, y añadir una guarda extra alrededor, de modo que el estado tendría que reintentarse.
Hasta ahora he podido sortearlo así. Ten en cuenta que cuantas más condiciones y restricciones, más potente tendrá que ser tu CPU, ya que está en la escala de NP.
- peterus
Aplicaciones reales de TLA+: https://foundation.tlapl.us/industry/index.html.
El artículo de Intel muestra cómo se aplicó TLA+ como paso previo a escribir la descripción del hardware. No estoy seguro de si llegó a cuajar, parece que hoy en día se usan otras herramientas, ¿alguien aquí en la industria VLSI lo sabe?
- pron
Me encanta TLA+ para describir sistemas de forma precisa pero concisa y razonar sobre ellos. Pero como alguien que lleva muchos años usando métodos formales para ayudar al desarrollo de software, toda esta industria alrededor de herramientas para conectar un lenguaje matemático tan maravilloso y otros como Lean con la IA, hasta el punto de ocultar el razonamiento a las personas, me confunde.
Probar que los programas son correctos de extremo a extremo (es decir, del código a propiedades de alto nivel) —como esta empresa y otras pretenden hacer— es tan difícil que los humanos solo han podido hacerlo para programas muy pequeños (~10KLOC) e incluso entonces, en casos muy especializados, donde los programas se han escrito de una manera extra simple (a menudo a costa del rendimiento, porque el rendimiento a menudo requiere algoritmos más complicados). Si la IA llega a ser al menos un orden de magnitud más capaz que los humanos en desarrollo de software, que es lo que se requerirá para esta tarea, ¿necesitaría nuestra ayuda para escribir diversas herramientas e infraestructuras que ayuden con la tarea? Después de todo, escribir estas herramientas es mucho más fácil que usarlas para ese objetivo, así que no entiendo la hipótesis que subyace a la capacidad de la IA aquí.
Esta empresa dice: están "desarrollando los marcos agénticos para hacer que estas garantías de corrección sean accesibles a todos los ingenieros de software". ¡Pero desarrollar todo eso es la parte fácil! Si la IA puede hacer la parte difícil, ¿por qué necesita nuestra ayuda para hacer esto accesible? ¡Seguro que puede encontrar la manera de hacer esa parte fácil por sí misma! Es como decir: "Pronto tendremos una máquina qu […]"
- bsenftner
Tardé 10 minutos en encontrar esto: TLA+ es un lenguaje de especificación formal desarrollado para diseñar, modelar, documentar y verificar sistemas reactivos.