El caso contra la verificación formal, 50 años después
La verificación formal del software se reconsidera a la luz de una famosa crítica de 1979, y muchos sostienen que, aunque las pruebas de extremo a extremo siguen siendo impracticables para sistemas reales y desordenados, la verificación dirigida de componentes críticos (p. ej., almacenes de datos distribuidos, compiladores, motores de políticas) es a la vez viable y valiosa. Los comentaristas destacan que especificar el comportamiento con rigor suele ser más difícil que escribir código, que la brecha modelo–código y la evolución de los requisitos limitan el alcance de las pruebas, y que la mayoría de los fallos reales surgen de especificaciones defectuosas o incoherentes más que de errores de implementación. Hay un optimismo prudente de que sistemas de tipos potentes, mejores herramientas y la ayuda de la IA puedan hacer los métodos formales más accesibles, pero también preocupación de que las pruebas puedan fosilizar malos diseños y de que los incentivos económicos sigan favoreciendo un software “suficientemente bueno” frente a la corrección garantizada matemáticamente.
Alcance y practicidad de la verificación formal
- Muchos consideran que la verificación de sistemas completos es intratable para productos desordenados y en evolución (p. ej., redes sociales, GUIs), pero coinciden en que verificar subsistemas y propiedades específicas es valioso.
- Las GUIs se consideran especialmente difíciles de especificar; algunos mencionan enfoques de GUI basados en restricciones como más cercanos a las especificaciones, principalmente para evitar errores obvios de la interfaz.
- Varios comentarios subrayan que no hace falta un enfoque de “todo o nada”: verificar permisos, la idempotencia de APIs, la consistencia distribuida y propiedades de no pérdida de datos ya es muy útil.
Verificación formal vs. pruebas
- La verificación se presenta como la garantía de propiedades para todas las ejecuciones, mientras que las pruebas muestrean ejecuciones.
- Se discuten las pruebas basadas en propiedades y las pruebas por mutación como técnicas intermedias; el fuzzing y las pruebas aleatorias se benefician de especificaciones claras.
- Algunos argumentan que deberíamos pensar en los métodos formales como “pruebas con esteroides”, no como un reemplazo.
Especificaciones: beneficios, dificultad y corrección
- Hay desacuerdo sobre si las especificaciones son más fáciles de entender que el código: algunos encuentran las especificaciones formales más concisas y más cercanas a la intención; otros las consideran más difíciles que las implementaciones.
- Se citan ejemplos históricos (operaciones de punto flotante, compresión, sistemas de archivos, bases de datos, redes) donde las especificaciones son simples y las implementaciones complejas.
- Un largo subhilo sobre “ordenar” ilustra cómo especificaciones aparentemente triviales pueden equivocarse de forma sutil, reforzando que escribir especificaciones correctas en sí mismo es difícil.
- Se plantea la pregunta: ¿por qué asumir que la especificación es más correcta que el programa? Las respuestas: comprobar suele ser más fácil que construir; las especificaciones pueden ser más simples; pero los errores en las especificaciones son reales y deben tratarse como bugs.
Economía, incentivos y regulación
- Las economías de tipo hardware (los bugs cuestan millones) justifican una verificación intensiva; el software suele depender en cambio de parches baratos.
- Algunos sostienen que ya existe software robusto allí donde los compradores pagan por él (bancos, aviación); otros señalan que el software de consumo típico sigue siendo defectuoso.
- Preocupa que los “sellos de verificación” regulatorios puedan convertirse en sellos burocráticos sin mejoras reales de calidad.
IA, herramientas y la brecha modelo–código
- Las limitaciones del pasado incluían notaciones pobres y cómputo insuficiente; los modernos solucionadores SAT/SMT, asistentes de pruebas y LLMs alivian parte de la carga.
- La IA actualmente es más eficaz en manos expertas; existe la esperanza de que los agentes terminen generando especificaciones y pruebas para módulos profundos con invariantes simples.
- La brecha modelo–código (p. ej., una especificación en TLA+ frente a código en Rust) se considera un problema central; las mitigaciones sugeridas incluyen:
- Asistentes de pruebas que generen código ejecutable.
- Lenguajes y ecosistemas (p. ej., SPARK/Ada, sistemas de tipos más ricos, motores de políticas verificados) donde especificaciones y código estén estrechamente integrados.
- Algunos temen que las pruebas y los tests de grano fino congelen abstracciones deficientes y dificulten la refactorización.
Requisitos vs. implementación
- Varios participantes argumentan que, en muchos proyectos reales, los principales fallos son requisitos inconsistentes o imposibles, no código incorrecto.
- Sugieren que la mayor necesidad son herramientas que ayuden a formalizar y verificar requisitos frente a restricciones técnicas y de negocio, no solo implementaciones.