Las especificaciones formales no existen para la mayoría del software

Artículo explicativo sobre por qué los métodos formales de verificación no pueden aplicarse de forma generalizada al software actual. El autor parte de una hipótesis central: una vez que se dispone de una especificación formal de calidad, verificar un sistema resulta costoso pero no difícil; el verdadero cuello de botella es la ausencia de tales especificaciones. Sistemas como compiladores, bibliotecas criptográficas, analizadores sintácticos y micronúcleos se han verificado con éxito precisamente porque admiten una formalización natural. Sin embargo, la mayoría del software del mundo real —desde navegadores web hasta procesadores de texto, incluido el propio formato PDF— carece de una especificación formal coherente. Las organizaciones manejan en su lugar especificaciones parciales e informales: presentaciones de dos diapositivas o documentos de requisitos de 7.000 páginas en prosa semiestructurada que no coinciden entre sí. Escribir una especificación formal exige una visión de arriba abajo que los ingenieros rara vez tienen, y muchos casos prácticos simplemente no pueden formalizarse de manera precisa. El texto ilustra esta brecha con el caso de PDF: aunque existe un estándar ISO mantenido por la PDF Association y múltiples implementaciones, no hay consenso sobre qué deben hacer los lectores de PDF, ni una definición clara de documento inseguro. La consecuencia es que la verificación formal seguirá siendo un nicho hasta que se resuelva el problema previo de poder especificar formalmente los sistemas.