¿Por qué la gente no usa métodos formales? (2019)
Los métodos formales para demostrar la corrección del software siguen siendo raros en el desarrollo cotidiano, en gran parte porque son difíciles de aprender, costosos de aplicar y a menudo se consideran innecesarios para aplicaciones de bajo riesgo como apps CRUD o plataformas sociales. Los comentaristas destacan que las técnicas rigurosas se adoptan sobre todo donde los fallos son extremadamente costosos (por ejemplo, diseño de hardware, bases de datos, finanzas, sistemas críticos), y que las formas ligeras como los sistemas de tipos, los linters y la verificación parcial son el compromiso más práctico. Varios sostienen que las herramientas de IA y una mejor instrumentación podrían reducir la barrera de entrada, pero subrayan que las pruebas formales siguen desplazando el problema a escribir especificaciones precisas, que pueden ser tan complejas y propensas a errores como el propio código.
Valor percibido y contexto empresarial
- Muchos sostienen que los métodos formales rara vez justifican su costo: la mayor parte del software es CRUD de bajo riesgo, prototipos o aplicaciones empresariales cambiantes en las que iterar rápido supera a las pruebas rigurosas.
- Se ve un mayor retorno de la inversión en infraestructuras y dominios críticos para la seguridad (bases de datos, sistemas de archivos, hardware, finanzas, criptografía, aviónica, medicina, DeFi), pero incluso allí la adopción es desigual.
- Algunos ven el infrauso como un síntoma de mala gestión del riesgo y de una cultura de “moverse rápido”; otros lo enmarcan más simplemente como una optimización racional del ROI.
Dificultad, educación y cultura
- Un tema recurrente: los métodos formales son difíciles de aprender, exigen mucho intelectualmente y están mal explicados; muchos ingenieros se sienten intimidados o no están interesados.
- Existe confusión sobre qué método usar; la gente quiere un “segundo mejor para todo” en lugar de un zoológico de técnicas.
- Quienes defienden los métodos formales informan de resistencia dentro de las empresas y a menudo los “introducen por la puerta de atrás” en su flujo de trabajo.
Especificaciones frente a código y límites
- Varios comentarios subrayan que las especificaciones pueden ser tan complejas como el código; los errores pueden simplemente pasar de la implementación a la especificación.
- La ordenación se usa para ilustrar lo sutil que es una especificación “completa” (debe capturar el orden, la longitud, la permutación, los duplicados y los empates).
- Los métodos formales se consideran un complemento de las pruebas, no un reemplazo; ambos dependen en última instancia de la comprensión humana de los requisitos.
Tipos, verificación parcial y técnicas pragmáticas
- Muchos señalan que los sistemas de tipos, los linters y análisis relacionados ya se usan ampliamente como “métodos formales ligeros”.
- Hay debate sobre dónde termina la “comprobación de tipos” y dónde empieza la “verificación formal”, y algunos insisten en que las restricciones de estilo refinamiento son el mínimo.
- La verificación parcial (por ejemplo, demostrar propiedades clave o pequeños componentes puros) se presenta como algo práctico, especialmente para bibliotecas, códecs y algoritmos de concurrencia.
Herramientas, ejemplos y estudios de caso
- Las herramientas se perciben como fragmentadas y difíciles de abordar; la gente pide soluciones de código abierto, fáciles para principiantes, de referencia obligada, y ejemplos no triviales (p. ej., un editor de texto, una app de tareas).
- Según se informa, el hardware y algunas grandes empresas de software usan herramientas formales más pesadas; un profesional que reescribía un motor de base de datos en Rust usó model checking para demostrar la equivalencia de más de 1000 funciones y descubrió errores sutiles en componentes anteriores.
- Según se informa, algunos grandes proveedores de nube usan modelos formales para el diseño y la validación de telemetría, pero los detalles y el alcance son discutidos.
LLMs y direcciones futuras
- Varios especulan que los LLMs podrían cambiar la ecuación al:
- Generar masivamente pruebas o especificaciones candidatas, que son más baratas de verificar que de producir.
- Hacer viable que personas no expertas experimenten con herramientas como TLA+, Lean y otras.
- Otros advierten que alimentar especificaciones formalmente precisas a un modelo de caja negra reintroduce otra capa que también debe ser confiable o verificada.