TLA+ no puede verificar todo lo que promete la euforia actual
What TLA+ can and can't check
El entusiasmo por la verificación formal tras el hallazgo de race conditions con Opus ha generado expectativas exageradas. TLA+ es potente para invariantes y liveness, pero no puede expresar propiedades de alcanzabilidad, hiperpropiedades ni propiedades sobre tiempo real o punto flotante. El autor, veterano educador en TLA+, pide mesura: la herramienta no resolverá por sí sola el desarrollo de software agéntico.
Para verificar una propiedad, ¡necesitamos tener una propiedad que verificar! Entonces, ¿cuáles son las propiedades que TLA+ ni siquiera puede expresar?
- sourdecor
Descubrí Quint[0] gracias a este comentario[1] en HN. Quint es "un lenguaje de especificación ejecutable [que funciona en JavaScript] con herramientas encantadoras basadas en la lógica temporal de acciones (TLA)". Creo que es genial y cualquiera interesado en TLA+ debería echarle un vistazo.
- singron
Me encanta esto. Es genial leerlo si estás intentando usar TLA+ para algo.
En otra línea, otra cosa en la que TLA+ no es bueno es modelar atómicos y en particular semánticas de memoria débil o cualquier cosa que no sea secuencialmente consistente. Si traduces tu algoritmo a pcal, se ejecutará como si fuera secuencialmente consistente. Si necesitas modelar no-consistencia-secuencial, entonces eso debe explicitarse con lógica explícita en TLA+, lo cual probablemente sea demasiado complicado y propenso a errores para hacerlo a mano. Los modelos de memoria de C/C++/Rust permiten muchas cosas raras. Imagino que necesitas añadir cachés de lectura y búferes de escritura para cada variable con instrucciones de vaciado de caché en los puntos apropiados, pero quizá haya una forma más elegante de hacerlo.
Si usas Rust, tanto miri como loom tienen analizadores que pueden comprobar cierto comportamiento no secuencialmente consistente (y loom en realidad no implementa consistencia secuencial en absoluto).
- adamddev1
Gran artículo. La gente sigue diciendo "podemos simplemente escribir tests" o, más recientemente, "podemos usar verificación formal", pensando que son salvaguardas suficientes que podemos usar y luego relegar toda la implementación a los LLM. Pero el hecho es que las máquinas de adivinación probabilística no pueden salvarlos. La gente no puede escapar de la necesidad de entender realmente las cosas que construye.
- rrook
creo que parte de esto es una deficiencia de nuestros lenguajes de programación. en general, los lenguajes permiten la expresión de grafos parciales, lo que hace que el problema de verificación sea técnicamente desafiante. mi opinión es que un lenguaje que solo exponga semántica de grafo cerrado podría ayudar a cerrar la brecha entre el modelo y la implementación, aunque no sea absoluto.
- metabagel
¡Me encantan las notas al pie en línea!