Programación imperativa vs declarativa III (Demostración Automática de Teoremas)

¿Cuantas veces nos hemos encontrado (los programadores) con un bug “raro”, esa conjunción astral que hace que nuestro software, tras meses e incluso años sin mostrar síntomas de debilidad, cruja cual madera reseca por el paso del tiempo?. ¿Cómo demostrar al cliente que no fallará más?, ¿y si hay vidas de personas dependientes de la no existencia de errores en un software como en el caso de Karen Sandler?.

¿Te habías fijado que en cuestión de software no es posible asegurar la ausencia de bugs?. Una vez escrito un código, todas las estrategias tradicionales se basan en la repetición de los procesos de verificación (eg. el código que ha escrito un programador es revisado por otros tantos) o en test que sólo pueden validar una parte muy pequeña del dominio funcional del proceso (eg. una función para sumar dos enteros de 32 bits posee un dominio de 2⁶⁴ elementos, revisarlos todos le llevaría a un procesador a 3GHz 195 años ¡y es una suma!).

¿Será la Demostración Automática de Teoremas la solución a todos los males?.


[...]
>>> Ver artículo original completo en: http://www.genbetadev.com