Un investigador en métodos formales relata cómo una prueba con la que estuvo meses torturándose casi se viene abajo por un error de signo en el código que, paradójicamente, el comprobador aceptó durante meses sin chistar. El episodio, sucedido durante la fase de rebuttal de un artículo sobre verificación de muestreadores exactos para distribuciones continuas, sirve como advertencia sobre los riesgos de confiar ciegamente en herramientas automatizadas, ahora que la inteligencia artificial permite producir pruebas y artefactos a granel.
El artículo en cuestión, titulado "Verifying Exact Samplers for Continuous Distributions with a Discrete Program Logic", demuestra cómo aplicar técnicas de lógica de programas para verificar implementaciones de números reales mediante bitstreams perezosos, usando el framework Iris en Rocq. La pieza fue aceptada inicialmente, pero al comprobar la terminación con una herramienta externa, Total Eris, el autor descubrió que su función IsLessThanDyadic no comparaba aproximaciones cada vez más finas del número diádico, sino cada vez más groseras, por culpa de un error de signo. El programa, en realidad, no terminaba.
La trampa radicaba en que la inducción de Loeb, principio central de la lógica usada, asume que el programa sigue trazas terminantes, de modo que una demostración correcta y una demostración vacía por no terminación resultan indistinguibles mientras no se cierre la hipótesis final. Como el autor había memorizado cada línea de su código tras meses de trabajo manual, pudo localizar y corregir el fallo en pocas horas y presentar la rebuttal a tiempo. La moraleja es clara: los métodos formales siguen siendo territorio de expertos, y cuando un artefacto generado a ciegas no encaja con el texto del artículo, el olfato de quien ha sudado la prueba sigue siendo insustituible.