Las preguntas que haces son en realidad bastante diferentes.
Sin embargo, no estoy seguro de hasta qué punto esto se aplica a los programas operativos del mundo real como los sistemas operativos. ¿Estos tipos de programas necesitan toda la fuerza de la integridad de Turing?
Se necesita muy poco para que un modelo de computación se complete en Turing. Por ejemplo, varios modelos con contadores pueden simular máquinas de Turing. Si cree que su software requiere más de dos contadores que puede manipular arbitrariamente, está utilizando un lenguaje completo de Turing. Aunque los enteros de la máquina están limitados a priori, las estructuras de datos asignadas al montón generalmente no lo están. Si su software necesita listas, árboles y otros datos asignados dinámicamente, está utilizando un lenguaje completo de Turing.
¿Existen modelos más simples de cómputo (como PR) en los que podrían escribirse estas aplicaciones? Si es así, ¿en qué medida esto permite la capacidad de decisión de la corrección del programa?
Es importante reconocer que no queremos verificar las propiedades arbitrarias de nuestro software. La comprobación de propiedades muy específicas y estrechas (sin desbordamientos de búfer, sin desreferencias de puntero nulo, sin bucles infinitos, etc.) mejora enormemente la calidad y la usabilidad del software. En teoría, tales problemas aún son indecidibles. En la práctica, enfocarnos en propiedades específicas nos permite descubrir estructuras en nuestros programas que a menudo podemos explotar para resolver el problema.
En particular, puede modificar su pregunta original para
¿Existe una abstracción de mi software que pueda analizar eficientemente en un modelo completo que no sea de Turing?
Una abstracción es un modelo que incluye el comportamiento del software original y posiblemente muchos comportamientos adicionales. Hay modelos como máquinas de un contador o sistemas pushdown que no están completos y que podemos analizar. El enfoque estándar en la verificación de programas con herramientas automatizadas es construir una abstracción en dicho modelo y verificarla algorítmicamente.
Hay aplicaciones en las que las personas se preocupan por las propiedades sofisticadas de su hardware o software. Las compañías de hardware quieren que sus chips implementen correctamente algoritmos aritméticos, las compañías automotrices y de aviónica quieren un software certificablemente correcto. Si es tan importante, es mejor usar un ser humano (entrenado).