Métodos formales y el futuro de la programación
El papel de los métodos formales con GenAI
- Varios comentarios sostienen que es más probable que GenAI acelere los métodos formales que al revés: la IA puede generar pruebas, especificaciones y andamiaje repetitivos.
- Idea: los humanos se centran en especificaciones de alto nivel; los LLM generan código y/o pruebas desordenadas, mientras comprobadores mecánicos garantizan la corrección.
- Otros señalan que las pruebas y los artefactos de verificación generados por LLMs son actualmente costosos, frágiles y todavía requieren expertos en métodos formales para guiarlos.
Coste, complejidad y límites de las especificaciones
- Varios participantes dicen que las especificaciones formales completas para sistemas no triviales suelen ser más grandes y complejas que la implementación, y pueden ser más opacas que el código.
- Los métodos formales garantizan solo la consistencia entre la especificación y la implementación; no garantizan que la especificación refleje la realidad o las condiciones cambiantes del negocio o del mercado.
- Existe la preocupación de que los sistemas rigurosos empujen a la gente a “rodearlos” (analogía con el borrow checker de Rust), o de que modelos demasiado ajustados solo refinen una visión del mundo equivocada.
Dónde encajan los métodos formales (y dónde no)
- Hay un consenso fuerte en que los métodos formales brillan donde la semántica es clara: kernels, protocolos, parsers, compiladores, criptografía, primitivas de concurrencia y trading crítico para la seguridad.
- Muchos argumentan que son un “lujo” justificado sobre todo en dominios de alto riesgo o alto volumen; para startups y productos exploratorios, puede ser más apropiada una “programación ofensiva” rápida.
- Algunos señalan que incluso las UIs y muchas capas de aplicación a menudo pueden modelarse como máquinas de estados y beneficiarse de especificaciones, aunque los objetivos de UX de nivel superior siguen siendo difusos.
Métodos formales frente a tests y pruebas basadas en propiedades
- Distinción clave: los tests y las pruebas basadas en propiedades muestrean comportamientos; los métodos formales buscan demostrar propiedades para todas las entradas y todas las ejecuciones.
- Sin embargo, escribir propiedades precisas puede parecerse a implementar de nuevo la función, y siguen existiendo errores sutiles en las especificaciones (por ejemplo, definiciones de espacios en blanco Unicode, desbordamiento de enteros).
Herramientas, lenguajes y flujos de trabajo
- Se habla de Lean, Coq, TLA+, Dafny, SPARK/Ada, esfuerzos de verificación en Rust y enfoques de tipos-como-pruebas en lenguajes convencionales.
- Varios enfatizan integrar especificaciones y pruebas directamente en la sintaxis del lenguaje de programación para evitar la “falta de correspondencia de impedancias”.
- Algunos son optimistas sobre el emergente “desarrollo guiado por especificaciones” y sistemas de tipos más fuertes como punto intermedio práctico; otros dudan de que los métodos formales lleguen a dominar alguna vez la programación cotidiana.