Métodos formales y el futuro de la programación: qué vale la pena probar y dónde está el techo
Hay una conversación que se repite en ciclos de tres o cuatro años. Alguien publica que los formal methods —verificación formal, especificación matemática, model checking— son la respuesta a los bugs que seguimos cometiendo después de décadas de avance en herramientas. El hilo de HN se llena de comentarios de personas que usaron TLA+ en sistemas distribuidos, de otras que intentaron Alloy en un proyecto real y lo abandonaron a la segunda semana, y de unas pocas que dicen que en AWS o en Microsoft ya corren esto en producción hace años.
El problema no es que la conversación sea falsa. El problema es que, cada vez que la leo, siento que está incompleta de la misma manera: habla del potencial sin hablar del costo de instalación, de los prerrequisitos de equipo y de los casos donde la verificación formal no escala —no conceptualmente, sino operativamente, en un equipo de cinco personas con un deadline real.
Mi tesis concreta: los formal methods señalan un problema genuino que TypeScript, tests y linters no resuelven del todo. Pero convertir eso en una decisión técnica requiere saber exactamente qué compra cada herramienta y a qué precio. Repetir "deberíamos usarlo" sin esa matriz no es criterio técnico, es hype con mejor vocabulario.
