Entrevistas
Gabriela Moreira, CEO de Quint en Informal Systems – Serie de entrevistas
Gabriela Moreira, CEO de Quint en Informal Systems, es una ingeniera de investigación especializada en lenguajes de programación y métodos formales, con un enfoque fuerte en la creación de herramientas que hacen que la verificación de sistemas complejos sea más accesible para los ingenieros. Dirige el desarrollo de Quint, un lenguaje de especificación ejecutable moderno basado en TLA+, donde continúa manteniendo y evolucionando el lenguaje y sus herramientas. Su trabajo abarca la verificación formal, el análisis estático y las herramientas de desarrollo, y también ha contribuido a la academia enseñando métodos formales, reflejando una combinación de ingeniería práctica y profundidad teórica.
Quint, desarrollado y mantenido en Informal Systems, es un lenguaje de especificación moderno diseñado para modelar, probar y verificar sistemas complejos como redes distribuidas, blockchains y bases de datos. Construido sobre los fundamentos de la Lógica Temporal de Acciones (TLA), Quint introduce una sintaxis más amigable para los desarrolladores, junto con herramientas avanzadas como comprobación de tipos, simulación y verificación de modelos, lo que permite a los ingenieros detectar fallos del sistema antes de su implementación. La plataforma enfatiza las especificaciones ejecutables, lo que permite a los desarrolladores no solo describir el comportamiento del sistema, sino también probar y explorarlo activamente, cerrando la brecha entre la corrección teórica y la implementación en el mundo real.
Volviendo al principio, ¿qué despertó inicialmente su interés en la programación, y cómo llegó a trabajar en métodos formales y sistemas distribuidos?
Era una ávida jugadora con una mala computadora, y me di cuenta de que disfrutaba arreglando los problemas y haciéndola funcionar. Me inscribí en ciencias de la computación y me atrajo la teoría y los compiladores.
En 2015, me presentaron concursos de programación. En ellos, generalmente obtienes algunos ejemplos de entrada y salida esperada, y escribes código que resuelve el problema y funciona para esos ejemplos. Sin embargo, después de enviarlo para su evaluación, el código se prueba con muchos más ejemplos más allá de los que se muestran. Esa realización de que el código podría funcionar para los escenarios que veo o pienso, pero aún fallar en casos que no he considerado, convirtió la programación en un tipo de desafío del que me enamoré.
Trabajando en la industria, me atrajeron rápidamente los sistemas distribuidos, donde teníamos que considerar diferentes ordenaciones de mensajes que podrían llegar, diferentes modos de fallo y un mundo de comportamientos ocultos. En 2018, un colega me presentó un lenguaje de especificación formal llamado TLA+. Me enganché. Inmediatamente comencé a construir herramientas alrededor de TLA+ y he estado trabajando en este espacio desde entonces.
Ha construido su carrera alrededor de métodos formales y lenguajes de programación, desde su trabajo temprano en herramientas basadas en la Lógica Temporal de Acciones (TLA+) hasta liderar el desarrollo de Quint en Informal Systems. ¿Qué la motivó a centrarse en hacer que la verificación formal sea más accesible, y cómo ha dado forma al diseño de Quint?
TLA+ es demasiado bueno como para no ser utilizado extensivamente en la industria. Todavía era bastante junior cuando aprendí sobre él, y me uní a esas llamadas con mis colegas de trabajo para tratar de encontrar soluciones juntos, y constantemente encontraba escenarios en los que nuestras soluciones fallarían. Sin embargo, siempre era la última línea de defensa contra esos escenarios en la mayoría de los casos. Me di cuenta de que debía haber una mejor manera, menos costosa y más valiosa, de resolver esos escenarios. Así que comencé mi viaje académico hacia ello, lo que me llevó a Informal Systems y Quint.
Quint no se concibió originalmente como un producto. Lo construimos por necesidad en Informal Systems. Estábamos escribiendo especificaciones TLA+ para sistemas que necesitábamos confiar más de lo que hacíamos, pero que no se expandían más allá de un pequeño grupo de personas, ya que la sintaxis era demasiado aterradora con demasiados símbolos matemáticos, y las herramientas no cumplían con las expectativas básicas de la gente. Les mostrábamos a los colegas y colaboradores externos: “miren esta cosa increíble que hice”, pero no podían leerla, y no tenían tiempo para aprender una nueva herramienta.
Las decisiones de diseño en Quint siguen directamente de esa experiencia. El lenguaje es fácil de leer y recordar. La primera cosa que construimos fue una extensión de VSCode que resalta los errores a medida que escribe. Tiene tipos y modos distintos para separar capas explícitamente. Tiene un REPL para que puedas explorar interactivamente, y un simulador para que puedas obtener retroalimentación rápida e iterar. Exporta trazas a un formato JSON estandarizado que es fácil de parsear para las máquinas. Estas eran cosas que los programadores ya esperaban de sus herramientas y que necesitábamos nosotros. La verificación subyacente es la misma lógica que TLA+.
Estoy obsesionada con hacer que los métodos formales sean más accesibles, y enviar herramientas es emocionante, pero el impacto real solo se siente si los equipos de ingeniería realmente las utilizan. Todavía hay un delta entre lo que las herramientas pueden hacer y lo útiles que parecen a los desarrolladores, y estoy trabajando para cerrar esa brecha.
Para los lectores que no están familiarizados con ello, ¿cómo explicaría qué es Quint y por qué se necesitaba un nuevo lenguaje de especificación junto con herramientas existentes como TLA+?
La mayoría de las especificaciones son documentación. Escribe lo que el sistema debe hacer, y lo verificas leyéndolo. El problema es que la documentación está mal de maneras que no se pueden detectar mecánicamente: nombres no definidos, comportamiento ambiguo, suposiciones implícitas. Generalmente, te enteras durante la implementación o en producción.
Una especificación de Quint es algo que se ejecuta. Modelas el sistema como una máquina de estado, defines las propiedades que debe satisfacer, y ejecutas o verificas el modelo. Si hay una violación, obtienes un contraejemplo que muestra exactamente la secuencia de pasos que lo desencadena. Eso cambia cuándo y cómo barato es detectar un error de diseño.
TLA+ siempre pudo hacer esto. Quint lo hace práctico para ingenieros que no son ya especialistas en lógica temporal.
Quint está diseñado para cerrar la brecha entre métodos formales y ingeniería de software cotidiana. ¿Cuáles fueron las barreras de usabilidad más grandes que intentó eliminar en comparación con los enfoques tradicionales?
Honestamente, la barrera de usabilidad más grande fue la sintaxis. Eso es por lo que empezamos con la sintaxis. Después de abordar eso, pudimos centrarnos más en otros factores. El sistema de tipos y efectos de Quint vino a señalarizar tantos errores como fuera posible antes de incluso comenzar el proceso de verificación regular, y la gente valoró eso mucho. Llevó a escribir especificaciones de mayor calidad que incluso más personas podían leer. Lo integramos todo en editores, y ofrecimos la funcionalidad básica que todos los desarrolladores tienen derecho a esperar.
El impacto más grande después de eso fue nuestro simulador. Comenzó como una forma de ofrecer a la gente una retroalimentación inicial sobre el comportamiento de su sistema, como un desarrollador quiere poder, de alguna manera, ejecutar el código después de escribirlo. Luego resultó ser extremadamente valioso como una forma de obtener confianza en especificaciones que son demasiado grandes para que la verificación las maneje, ya que la experiencia de adaptar una especificación para hacerla factible para la verificación no debe darse por sentada. Nuestro simulador hizo que la confianza fuera más accesible y lo hemos estado utilizando extensivamente en muchos proyectos.
Mi mayor dolor de cabeza con la sintaxis de TLA+ fue cómo frecuentemente mezclaba mis barras inclinadas y barras normales, y necesitas escribir esas mucho. Me gusta la sintaxis de Quint mucho mejor, pero lo que realmente me hace imposible regresar es toda la herramienta.
Una de las fortalezas de Quint es su capacidad para modelar y probar sistemas distribuidos antes de su implementación. ¿Cómo cambia esto la forma en que los ingenieros deben pensar sobre la construcción de sistemas como blockchains o infraestructura en tiempo real?
El cambio más grande es mover la validación más temprano. Leslie Lamport, creador de TLA+, compara escribir especificaciones antes del código con dibujar planos antes de la construcción. Incluso si ya has construido algo sin un plano, todavía es una buena idea escribir uno ahora y usarlo para informar tus cambios posteriores.
En la industria del software, usamos archivos de markdown y pizarras. Tal vez puedas compararlo con tratar de describir textualmente un edificio. Funciona, pero ¿sabrías si el tamaño de las paredes suma? Quint ofrece una forma de describir sistemas donde puedes ser tan de alto nivel como desees, y obtener información sobre su comportamiento y corrección.
Quint se basa en los fundamentos de TLA+, que se utiliza ampliamente para describir sistemas distribuidos. ¿Cómo equilibró mantener ese rigor teórico mientras hacía que el lenguaje sea más amigable para los desarrolladores?
La decisión clave fue restringir Quint a un fragmento de TLA (la lógica detrás de TLA+) en lugar de exponer todo lo que la lógica permite. TLA es muy expresiva, y parte de esa expresividad incluye operadores que no son compatibles con ninguna herramienta, y permite combinaciones que la gente entiende y usa mal, lo que hace que sea realmente difícil depurar. Tomamos una decisión deliberada: nos quedamos con lo que la mayoría de las especificaciones realistas necesitan, y evitamos lo que tiene potencial de confusión.
El sistema de tipos y efectos agrega restricciones, pero restricciones que son útiles. Evitan una clase completa de errores de especificación que no son divertidos cuando se encuentran después de que la verificación ya está en ejecución. Los tipos son casi enteramente inferidos y los efectos están ocultos para los usuarios, así que esto agrega valor con ninguna fricción.
Antes de que aprendiera sobre la existencia de TLA+, estaba haciendo investigación en sistemas de tipos, lo que significa que el verificador de tipos de Quint probablemente fue mi componente favorito para escribir. Recuerdo bebiendo un café con sabor a Paçoca en mis primeros meses en Informal mientras revisaba algún papel sobre el sistema de tipos y pensando “mi vida es increíble”.
Hacer que el lenguaje sea bueno para usar mientras mantiene la correspondencia con TLA+ (ya que las especificaciones de Quint se pueden transpilar a TLA+) fue un ejercicio de lenguaje de programación, y las discusiones con el equipo fueron el recurso más útil, seguido de la retroalimentación de los primeros usuarios. Todavía hay mejoras que queremos hacer, y puede que sea mi parte favorita del trabajo.
También ha trabajado en análisis estático y sistemas de tipos. ¿Cómo han influido esas experiencias en la comprobación de tipos de Quint, la herramienta y la experiencia general del desarrollador?
La lección más grande que aprendí en ese mundo es que no todos los lenguajes son iguales. Escucharás a la gente diciendo que es solo cuestión de aprender una nueva sintaxis, todos los mismos conceptos todavía se aplican, así que todos los lenguajes son iguales y es solo cuestión de gusto. Eso no es cierto. El campo de los lenguajes de programación tiene grandes investigadores que hacen un trabajo increíble para avanzar en este campo, y eso no es solo para hacer que un lenguaje se vea más bonito o más de su agrado.
La programación funcional se me presentó muy temprano, aprendí Haskell al mismo tiempo que aprendí C (mi primer lenguaje de programación), y estoy muy agradecida por eso. Esto es la base que me ayuda a ver que aislar las mutaciones de estado y la no determinismo en una capa delgada en Quint, y tener toda la complejidad en funciones puras, ayuda objetivamente en muchos factores, y no es solo cuestión de gusto. No creo que construir Quint hubiera sido productivo si los asuntos de gusto estuvieran sujetos a discusión con demasiada frecuencia.
Enseñar métodos formales como profesor le da una perspectiva única. ¿Cuáles son los conceptos erróneos más comunes que los ingenieros tienen sobre la verificación formal hoy en día?
Bueno, estaba enseñando a estudiantes de pregrado que estaban empezando en la industria. La gran mayoría de ellos nunca había oído hablar de métodos formales o verificación formal antes, así que no había conceptos erróneos. El plan de estudios se hizo de tal manera que la mayoría de ellos tampoco aprendieron sobre sistemas distribuidos, y sobre la mitad de ellos aprenderían sobre hilos en el mismo semestre. Solía decirles que me sentía como si les estuviera enseñando qué es un paraguas antes de que hubieran experimentado lluvia.
Estaba más motivada para enseñarles cómo los métodos formales y la especificación formal de un sistema pueden ayudarnos a razonar sobre soluciones y encontrar casos de borde que a hacer que pensaran que deberían verificar formalmente todos los programas que escribieran. Mi tarea final fue un entorno de juego de mesa donde diferentes órdenes que los jugadores podrían tomar y diferentes configuraciones tenían que ser tomadas en cuenta, tratando de imitar las dificultades que enfrentamos en los sistemas distribuidos tanto como pudiera. Funcionó al ser lo suficientemente difícil como para que tuvieran que usar las herramientas para encontrar casos de borde y mejorar sus soluciones para vencer a los monstruos al final. Espero que cuando enfrenten una situación similar en el trabajo algún día, recuerdenme. Algunos de ellos ya lo han hecho.
Hay un interés creciente en combinar la inteligencia artificial con el desarrollo de software. ¿Ve un papel para la inteligencia artificial en ayudar a los desarrolladores a escribir, validar o incluso generar especificaciones formales usando herramientas como Quint?
Un papel significativo, y ya está sucediendo. La ciencia de la computación es más grande que escribir código, y la inteligencia artificial abre la puerta a formas completamente nuevas de usar métodos formales. Los LLM son buenos para escribir especificaciones de Quint a partir de descripciones de lenguaje natural de un sistema y incluso código existente. El kit LLM de Quint tiene agentes de Claude Code que toman una descripción en inglés de un protocolo y producen una especificación de Quint que puedes ejecutar y verificar de inmediato.
Al mismo tiempo, Quint también ayuda a los desarrolladores a confiar en el código escrito con inteligencia artificial. Creo firmemente que la confianza necesita provenir de la comprensión, no de algún tipo de verificación mágica. Trabajar en una especificación de Quint que impulsa y verifica el código de implementación significa que los desarrolladores todavía pueden poseer y entender el comportamiento del sistema, abordando la deuda cognitiva que el uso de la inteligencia artificial puede crear y proporcionando formas más asertivas de validar el código generado.
Estamos utilizando LLM como herramientas de lenguaje que escriben definiciones precisas de Quint a partir de la intención de lenguaje natural, y luego damos las herramientas de Quint a la inteligencia artificial para que pueda lograr cosas que no puede hacer de manera fiable por sí sola, como encontrar casos de borde.
Mirando hacia adelante, ¿qué necesita suceder para que los métodos formales pasen de una adopción de nicho a una parte estándar del ciclo de vida de desarrollo de software?
Desde hace un tiempo, sé que las dos cosas de alto nivel que Quint necesita para una mayor adopción son un menor costo y un mayor valor. Creo que esto se aplica a muchas otras cosas también. Los métodos formales acaban de recibir un gran impulso en ambas cosas, con la inteligencia artificial reduciendo enormemente el costo de escribir especificaciones formales y también creando el entorno de falta de confianza y comprensión donde los métodos formales pueden ser los más impactantes y valiosos.
Con la inteligencia artificial cambiando lo que es nuestra profesión, al menos en alguna medida, espero que este cambio sea hacia decisiones de diseño de alto nivel y corrección de comportamiento, haciendo que los métodos formales sean una herramienta de todos los días; y no hacia que no entendamos ningún código o sistema más y pasemos todo nuestro tiempo revisando código generado por la inteligencia artificial sin ninguna herramienta para ayudarnos a razonar sobre ello.
Gracias por la entrevista perspicaz; los lectores interesados en aprender más sobre este lenguaje de especificación ejecutable para modelar y verificar sistemas complejos, incluyendo su herramienta y cómo empezar, pueden explorar Quint.
