Escribir software correcto es difícil: la matemática no basta
Why Writing Correct Software Is Hard
El artículo repasa resultados de la teoría de la computabilidad y la complejidad para argumentar que la corrección del software es intrínsecamente difícil. El teorema de la parada, el teorema de Rice y el teorema del castor ocupado muestran que no existe un algoritmo general para decidir si un programa termina o si cumple una propiedad no trivial. Incluso hay programas pequeños, de unos cientos de líneas, cuyo comportamiento no puede demostrarse formalmente. La corrección tiene un costo inevitable, como el costo energético de reducir la entropía.
Para el matemático no existe el Ignorabimus y, en mi opinión, tampoco para las ciencias naturales. ... La verdadera razón por la que nadie ha encontrado un problema irresoluble es, en mi opinión, que no hay ningún problema irresoluble.
- turbobutton
Creo que existe una distinción clara entre la corrección abstracta y matemática en el software y el funcionamiento en el mundo real. Cualquier software que procese entradas y proporcione flujos de trabajo complejos a los humanos tiene que lidiar necesariamente con las interminables vicisitudes de la realidad.
No digo que la corrección formal no tenga valor, pero lo importante es identificar cuándo es útil y cuándo da más problemas que beneficios...
- mpweiher
Creo que primero hay que definir qué es exactamente "correcto".
¿Correcto con respecto a una especificación formal?
¿Cómo sabemos que la especificación es "correcta"? ¿Por definición?
- johnbender
Por lo que puedo ver, el artículo confunde erróneamente el Teorema de Rice con la idea de que uno no puede probar algo sobre el pequeño programa generado por Yedidiya y Aaronson, pero eso no es lo que nos dice el Teorema de Rice. En cambio, nos dice que no podemos idear un método general para determinar sí o no correctamente para todos los programas si un programa alcanza un punto dado.
Para un programa dado y una prueba única, se pueden probar muchas cosas o, si sobreaproximamos asumiendo que los bucles terminan, podemos probar muchas cosas de forma sólida con el riesgo de rechazar programas que a veces son correctos (por ejemplo, los sistemas de tipos).
Sin embargo, esto puede haber sido una peculiaridad del lenguaje o de mi interpretación.
- kodoman
Siempre me interesó la verificación formal, pero solo he escrito pruebas de juguete y programas derivados.
Es agradable ver esta discusión más antigua sobre el tema fuera de 'la IA hace Lean' y de las suposiciones de que la verificación formal es fácil o lo será para la IA y que puedes simplemente apagar el cerebro.
Construir programas que puedan verificarse en primer lugar es un problema de diseño difícil que requiere pensamiento real y una visión profunda del problema.
- tromp
> una máquina de Turing con 1919 estados de control que no se puede probar que termine (es decir, es "independiente de ZFC"). Esta máquina es tan pequeña que cabe cómodamente en un desafío 4K
Una pequeña objeción:
Un desafío 4K normalmente se refiere a código que cabe en 4KB, pero una codificación directa de una MT de 1919 estados ocupa 19192(2+11) = 49894 bits, o 6237 bytes, más de 6KB.
Sin embargo, las recientes optimizaciones impulsadas por IA han reducido el recuento a como máximo 215 estados, lo que cabe cómodamente en 1KB...
- nirinor
La parte más importante de una afirmación negativa es implícita: ¿qué suposiciones razonables podrían negar la afirmación?
Claro, por el teorema de Rice, ningún programa puede decidir si una función arbitraria siempre calcula la suma de sus dos entradas. Pero eso es solo porque estamos permitiendo implementaciones arbitrariamente difíciles de analizar de la función suma. Así que este teorema coexiste con el hecho de que las implementaciones simples de suma se pueden probar correctas.
Bajo esta luz, creo que la mejor conclusión es "para escribir software correcto en un tiempo razonable, debemos usar lenguajes y estilos de programación fáciles de analizar".
- bluGill
La verdadera pregunta es: para un programa típico, ¿lo probamos, aunque sabemos que hay programas que no podemos probar?
No me importan los ejemplos dados, me importa mi procesador de texto, mi navegador web y similares. ¿Podemos probarlos, poniendo límites al lenguaje de scripting?
- myrmidon
Me pareció interesante cómo el límite inferior del campeón de BB(6) (castor ocupado de 2 símbolos y 6 estados) data el artículo: da >10^36534, pero el campeón actual (mxdys 2025) es >10↑↑10↑↑10↑↑8 (10↑↑8 es una torre de potencias 10^10^10^10... ocho de alto, y la expresión se resuelve de derecha a izquierda, así que 10↑↑10↑↑8 ya es completamente inimaginablemente grande).