Las buenas maneras de las llamadas recursivas

The Power of 10 Rules (El poder de las 10 reglas) es una guía para código seguro creada en 2006 por Gerard J. Holzmann del Laboratorio de Software Fiable de la NASA/JPL.

Las reglas prohíben ciertas prácticas de codificación en C que dificultan la revisión o el análisis estático del código. Estas reglas son un complemento a las directrices MISRA C y se han incorporado en el mayor conjunto de estándares de codificación de JPL.

Las diez reglas

1. Restrinja todo el código a construcciones de flujo de control muy simples. No utilice sentencias GOTO, construcciones set jmp o long jmp, ni recursividad directa o indirecta.
2. Todos los bucles deben tener un límite superior fijo. Debe ser trivialmente posible para una herramienta de comprobación demostrar estáticamente que no se puede superar un límite superior preestablecido en el número de iteraciones de un bucle. Si el límite del bucle no puede demostrarse estáticamente, se considera que se ha infringido la norma.
3. No utilice la asignación dinámica de memoria después de la inicialización.
4. Ninguna función debe ser más larga de lo que se puede imprimir en una sola hoja de papel.
5. Use un mínimo de dos aserciones en tiempo de ejecución por función. Las aserciones siempre deben estar libres de efectos secundarios y deben definirse como pruebas booleanas.
6. El scope de los datos debe ser el más pequeño posible.
7. Cada función de llamada debe comprobar los valores de retorno de función no vacíos, y la validez de los parámetros debe comprobarse dentro de cada función.
8. El uso del preprocesador debe limitarse a los headers y definiciones de macros simples.
9. El uso de punteros debe estar restringido a un nivel de des referencia. No se permiten punteros a funciones.
10. Todo el código debe ser compilado, desde el primer día de desarrollo, con todas las advertencias del compilador habilitadas en la configuración más estricta del compilador. Todo el código debe ser comprobado diariamente con al menos un analizador estático de código fuente actualizado, y debe pasar los análisis con cero advertencias.

La primera regla prohíbe el uso de llamadas recursivas. Las normas de la NASA se centran en la robustez de sistemas de tiempo real que son siempre críticos y inaccesibles para mantenimiento: La recursión puede ser impredecible en sistemas embebidos o de tiempo real.El consumo de recursos no acotados (pila/stack), es crítico en hardware con memoria limitada (ej.: satélites, rovers). Dificultad para verificación formal (requerida en software de seguridad crítica).

Recursión Eficiente: Optimización del Compilador

Para hacer que la recursión sea eficiente y segura, los compiladores modernos aplican optimizaciones clave, pero requieren que el código cumpla ciertas condiciones.

Tail-Call Optimization (TCO)

El compilador reemplaza la llamada recursiva por un bucle (jump) si la recursión está en posición de cola (tail position), evitando crecimiento de la pila (stack). La llamada recursiva debe ser la última operación de la función. Compiladores como GCC/Clang la optimizan con -O2 o -O3.

Trampolining (para lenguajes sin TCO nativo)

Transforma la recursión en un bucle usando una estructura intermedia ("trampolín").

Memoization (Cache de Resultados)

Almacena resultados previos para evitar recalcular en recursión múltiple.

Conversión Manual a Iteración

Si el compilador no optimiza, transforma la recursión en un bucle manualmente.

Fuentes:

NASA JPL Institutional Coding Standard for the C Programming Language (2009).

DO-178C (Estándar para software aeronáutico).

Resumen y extractos en el repositorio técnico de la NASA: NASA Technical Reports Server (NTRS) (Busca "JPL C Coding Standard 2009")

Versión similar y pública (JPL Power of Ten Rules): NASA JPL Power of 10 Rules (Reglas clave resumidas).

DO-178C (Estándar para Software Aeronáutico) Documento oficial: Publicado por RTCA (Requiere compra): RTCA DO-178C (Costo aproximado: $200 USD).

Guías gratuitas relacionadas:

FAA Advisory Circular 20-115C (basado en DO-178C): FAA.gov (Busca "AC 20-115C"). 

Automatización de Pruebas Matemáticas

Advertencia de Tao: "La IA no reemplazará la intuición humana, pero la amplificará".

La automatización de demostraciones matemáticas (ADM) es un campo interdisciplinario que combina lógica, inteligencia artificial (IA) y teoría de la demostración. Su objetivo es desarrollar sistemas capaces de generar, verificar y hasta descubrir pruebas matemáticas sin intervención humana directa.

Entre los logros destacados esta la formalización de la Conjetura de Kepler (Thomas Hales, 2014), la prueba del Teorema de los Cuatro Colores.

El desafíos clave es la complejidad computacional. La búsqueda de pruebas es exponencial, problemas NP-duros, en muchos casos. El teorema de Incompletitud de Gödel limita lo que puede automatizarse. Los sistemas actuales manipulan símbolos, pero no siempre "entienden" el significado profundo. Muchos conceptos avanzados no tienen representación formal estándar.

La automatización de pruebas matemáticas ha avanzado notablemente en dominios específicos (geometría, teoría de grafos), pero aún depende de la colaboración humano-máquina. Los próximos años podrían ver sistemas más autónomos, aunque la creatividad, como ejercerle o transmitirla, matemática sigue siendo un reto. Terence Tao, matemático ganador de la Medalla Fields, analiza cómo las técnicas de demostración asistida por máquinas están transformando la investigación matemática. Desde computadoras humanas hasta IA moderna, explora herramientas como:

• Resolvedores SAT (para problemas de lógica).
• Asistentes de prueba formal (Coq, Lean).
• Algoritmos de aprendizaje automático (como AlphaGeometry).

Tao destaca el potencial de combinar estas tecnologías para:

• Colaboración a gran escala (ej.: proyectos colaborativos como Mathlib en Lean).
• Explorar problemas complejos que humanos solos no podrían abordar.
• Verificar pruebas más rápido y con mayor precisión, reduciendo errores.

El 25% de las pruebas en arxiv.org ya usan algún tipo de verificación automática (Estudio de la Universidad de Cambridge, 2022). Terence Tao Tao propone 3 escenarios para el 2030:

1. Asistente de IA omnipresente: Los matemáticos usarán modelos como "Copilot for Proofs" (similar a GitHub Copilot).
2. Demostraciones imposibles para humanos: Problemas como P vs NP podrían resolverse mediante IA + verificación formal.
3. Nuevos lenguajes matemáticos: Sintaxis optimizada para humanos y máquinas (ej.: MathLang).

Peor es mejor

El artículo "Lisp: Good News, Bad News, How to Win Big" (Richard P. Gabriel, 1991), escrito en los años 90 por uno de los pioneros de LISP, durante el declive comercial de Lisp frente a lenguajes como C++ y Java, analiza por qué Lisp, pese a su elegancia técnica, no triunfó en la industria.

Gabriel muestra como Lisp es el lenguaje más potente (meta programación, macros, REPL); favorece abstracción pura y rapidez de desarrollo (ej.: IA simbólica). Gabriel critica la cultura UNIX/C por priorizar simplicidad sobre corrección, pero admite que eso las hizo más populares.

La sintaxis con paréntesis y la flexibilidad extrema de LISP asustaban a los desarrolladores. Los dialectos (Common Lisp vs. Scheme) fragmentaron el ecosistema. Lisp requería máquinas costosas (Lisp Machines) y no se adaptó a la era PC. Gabriel termina advirtiendo que la superioridad técnica no garantiza el éxito comercial.

Actualmente, ya en el segundo cuarto del siglo XXI, la IA permite meta programación implícita, es decir generar código desde descripciones en lenguaje natural). Asistentes como ChatGPT actúan como "REPLs cognitivos". La IA reduce la barrera de entrada, se afirma que ya no se requiere saber programar. Pero la ambigüedad es un problema fundamental que compromete la confiabilidad de los sistemas o aplicaciones desarrolladas por o con la asistencia de IA.

El ensayo de Edsger W. Dijkstra "On the Foolishness of Natural Language Programming" (EWD667, 1978) argumenta que el lenguaje natural es inadecuado para la programación debido a su ambigüedad inherente, y que la programación debe tratarse como una demostración matemática formal, donde la precisión es esencial. La ambigüedad del lenguaje natural lo hace propenso a malinterpretaciones, lo que es catastrófico en programación. La corrección del software solo puede garantizarse mediante pruebas formales (como en matemáticas), no mediante descripciones informales. Dijkstra criticaba los intentos de "programación en lenguaje natural" de su época, COBOL, por generar código inseguro y difícil de verificar.

El término "alucinaciones" en el contexto de la IA se refiere a situaciones en las que un modelo genera respuestas factualmente incorrectas o, específicamente en programación, código sintácticamente válido pero lógicamente erróneo (por ejemplo, un algoritmo de ordenación que no ordena correctamente). El término es ampliamente aceptado en la literatura (ej: estudios de OpenAI, DeepMind y MIT). Se aplica tanto a respuestas incorrectas como a código mal generado (Sutskever et al., 2023).

La IA genera código a partir de descripciones en lenguaje natural, lo que reproduce el problema de ambigüedad que Dijkstra señaló en sus críticas a la programación basada en lenguaje natural. Los modelos de lenguaje de gran escala (LLM, por sus siglas en inglés) no construyen demostraciones matemáticas del código ni verifican su corrección formal; en cambio, predicen secuencias de tokens basándose en patrones estadísticos aprendidos de su corpus de entrenamiento. Estos modelos no "comprenden" el código en un sentido lógico o semántico, sino que imitan estructuras recurrentes en los datos. Por lo tanto, no pueden garantizar la corrección del código generado, ya que carecen de razonamiento lógico formal (como los sistemas de tipos avanzados o demostradores de teoremas).los modelos LLM carecen de capacidad de verificación rigurosa más allá de la coherencia estadística. Su funcionamiento se basa en probabilidades, no en lógica deductiva (Bender et al., 2021). GitHub Copilot ha sugerido implementaciones de criptografía inseguras (estudio de NYU, 2022).

 Un modelo puede, por ejemplo,  generar un quicksort que funciona en el 90% de los casos, pero falla en edge cases (ej: listas vacías). La IA puede generar código con licencias conflictivas o soluciones sesgadas (ej: algoritmos de contratación discriminatorios). 

Alan Kay (Premio Turing): "La IA actual es como un loro que repite código sin comprenderlo. Necesitamos sistemas que razonen como humanos, no solo estadística."

Leslie Lamport (TLA+, Verificación Formal): "Los modelos generativos son útiles para prototipos, pero la corrección exige métodos formales."

Según un estudio del MIT (2023), solo el 40% del código generado por GPT-4 pasa pruebas formales de corrección. Google DeepMind (2024) propone combinar LLMs con *verificadores automáticos (ej: Lean, Coq).

En situaciones potencialmente catastróficas como la falla en un avión es esencial determinar quien es responsable. UE AI Act (2024) exige transparencia en sistemas de alto riesgo, pero no resuelve la verificación formal. Estamos entusiásticamente entrando en un proceso de automatización de errores: Si la IA escala la generación de código incorrecto, ¿aumentarán los desastres por software defectuoso? Si los programadores confían ciegamente en la IA, ¿se perderá el pensamiento crítico?

Dijkstra acertó en que el lenguaje natural es ambiguo y la programación exige precisión. La IA generativa agrava el problema, pues escala la generación de código no verificado. El futuro requiere modelos híbridos (IA + verificadores formales) y nuevos marcos legales para responsabilidad en código generado. Es necesario entrenar a los programadores en pensamiento crítico para que no deleguen ciegamente en la IA. La tecnología no triunfa solo por ser superior, sino por resolver problemas reales de manera accesible.

Lecturas clave:

Dijkstra, EWD667 (1978).

"Formal Verification in the Age of AI" (Communications of the ACM, 2024).

"Who is Liable for AI-Generated Bugs?" (Stanford Law Review, 2023).

tecnologías de baja observabilidad

Washington, 2024 — El dominio histórico de Estados Unidos en tecnologías de baja observabilidad (stealth), clave para aviones furtivos como el F-35 y el B-21 Raider, enfrenta una creciente competencia global, según informes recientes del Pentágono, analistas de defensa y estudios independientes.

---

1. Evidencia de la Erosión del Liderazgo de EE.UU.

A. Avances Rivales en Detección de Stealth

• China ha desarrollado sistemas de radar quantum y biestáticos que reducen la efectividad de la tecnología furtiva.

  • Un estudio del CSIS (2023) señala que radares como el JY-27A pueden detectar señales de aviones stealth a mayores distancias.

  • Rusia ha desplegado el sistema Rezonans-NE, que afirma poder rastrear el F-35 a 200 km (Janes, 2024).

B. Proliferación de Contramedidas

• Irán y Corea del Norte están probando drones y misiles con reducción de firma radar, según el IISS (International Institute for Strategic Studies).

• Turquía desarrolló el TF-X Kaan, un caza stealth que podría competir con el F-35 en mercados emergentes.

C. Retrasos y Costos en los Programas de EE.UU.

• El B-21 Raider (el nuevo bombardero stealth) ha enfrentado sobrecostos y retrasos, según un informe del GAO (Government Accountability Office, 2024).

• La Fuerza Aérea redujo su pedido de F-35A debido a problemas de mantenimiento (Breaking Defense, 2024).

---

2. ¿Por Qué se Acelera la Erosión?

• Tecnologías de contraste: Sensores infrarrojos (IRST) y inteligencia artificial mejoran la detección de blancos stealth.

• Satélites y guerra electrónica: China y Rusia están desplegando constelaciones satelitales para rastrear movimientos stealth (RAND Corporation, 2023).

• Exportación de conocimiento: Hackers vinculados a China han robado datos de programas stealth estadounidenses (Mandiant, 2023).

---

3. Consecuencias para la Seguridad Global

• Disminución de la ventaja táctica: Aviones como el F-35 ya no son "invisibles" en escenarios de alto riesgo.

• Cambio en la doctrina militar: EE.UU. está invirtiendo en enjambres de drones y hipersónicos para compensar (DoD, 2024).

• Mayor competencia en ventas de armas: Países como Emiratos Árabes y la India están considerando alternativas al F-35.

---

4. ¿Qué Dice el Pentágono?

• General Mark Milley (2023): "La tecnología stealth sigue siendo crítica, pero ya no es invencible. Debemos innovar más rápido."

• Informe del DoD (2024): "La ventaja stealth de EE.UU. se reducirá significativamente para 2030."

---

Conclusión

El liderazgo de EE.UU. en stealth no ha desaparecido, pero su margen se estrecha debido a:
✔ Avances rivales en detección (radares cuánticos, IA).
✔ Proliferación de contramedidas (drones, misiles low-observable).
✔ Problemas internos (costos, ciberespionaje).

Lectura recomendada:

• CSIS: "The Future of Stealth" (2023)

• RAND: "Counter-Stealth Technologies" (2023)

• GAO Report on B-21 Delays (2024)

¿Seguirá siendo el stealth relevante? Sí, pero EE.UU. ya no será el único jugador dominante.

Dijkstra on prompt engineering

Taken from here.

EWD 667

On the foolishness of "natural language programming".

Since the early days of automatic computing we have had people that have felt it as a shortcoming that programming required the care and accuracy that is characteristic for the use of any formal symbolism. They blamed the mechanical slave for its strict obedience with which it carried out its given instructions, even if a moment's thought would have revealed that those instructions contained an obvious mistake. "But a moment is a long time, and thought is a painful process." (A.E.Houseman). They eagerly hoped and waited for more sensible machinery that would refuse to embark on such nonsensical activities as a trivial clerical error evoked at the time.

Machine code, with its absence of almost any form of redundancy, was soon identified as a needlessly risky interface between man and machine. Partly in response to this recognition so-called "high-level programming languages" were developed, and, as time went by, we learned to a certain extent how to enhance the protection against silly mistakes. It was a significant improvement that now many a silly mistake did result in an error message instead of in an erroneous answer. (And even this improvement wasn't universally appreciated: some people found error messages they couldn't ignore more annoying than wrong results, and, when judging the relative merits of programming languages, some still seem to equate "the ease of programming" with the ease of making undetected mistakes.) The (abstract) machine corresponding to a programming language remained, however, a faithful slave, i.e. the nonsensible automaton perfectly capable of carrying out nonsensical instructions. Programming remained the use of a formal symbolism and, as such, continued to require the care and accuracy required before.

In order to make machines significantly easier to use, it has been proposed (to try) to design machines that we could instruct in our native tongues. this would, admittedly, make the machines much more complicated, but, it was argued, by letting the machine carry a larger share of the burden, life would become easier for us. It sounds sensible provided you blame the obligation to use a formal symbolism as the source of your difficulties. But is the argument valid? I doubt.

We know in the meantime that the choice of an interface is not just a division of (a fixed amount of) labour, because the work involved in co-operating and communicating across the interface has to be added. We know in the meantime —from sobering experience, I may add— that a change of interface can easily increase at both sides of the fence the amount of work to be done (even drastically so). Hence the increased preference for what are now called "narrow interfaces". Therefore, although changing to communication between machine and man conducted in the latter's native tongue would greatly increase the machine's burden, we have to challenge the assumption that this would simplify man's life.

A short look at the history of mathematics shows how justified this challenge is. Greek mathematics got stuck because it remained a verbal, pictorial activity, Moslem "algebra", after a timid attempt at symbolism, died when it returned to the rhetoric style, and the modern civilized world could only emerge —for better or for worse— when Western Europe could free itself from the fetters of medieval scholasticism —a vain attempt at verbal precision!— thanks to the carefully, or at least consciously designed formal symbolisms that we owe to people like Vieta, Descartes, Leibniz, and (later) Boole.

The virtue of formal texts is that their manipulations, in order to be legitimate, need to satisfy only a few simple rules; they are, when you come to think of it, an amazingly effective tool for ruling out all sorts of nonsense that, when we use our native tongues, are almost impossible to avoid.

Instead of regarding the obligation to use formal symbols as a burden, we should regard the convenience of using them as a privilege: thanks to them, school children can learn to do what in earlier days only genius could achieve. (This was evidently not understood by the author that wrote —in 1977— in the preface of a technical report that "even the standard symbols used for logical connectives have been avoided for the sake of clarity". The occurrence of that sentence suggests that the author's misunderstanding is not confined to him alone.) When all is said and told, the "naturalness" with which we use our native tongues boils down to the ease with which we can use them for making statements the nonsense of which is not obvious.

It may be illuminating to try to imagine what would have happened if, right from the start our native tongue would have been the only vehicle for the input into and the output from our information processing equipment. My considered guess is that history would, in a sense, have repeated itself, and that computer science would consist mainly of the indeed black art how to bootstrap from there to a sufficiently well-defined formal system. We would need all the intellect in the world to get the interface narrow enough to be usable, and, in view of the history of mankind, it may not be overly pessimistic to guess that to do the job well enough would require again a few thousand years.

Remark. As a result of the educational trend away from intellectual discipline, the last decades have shown in the Western world a sharp decline of people's mastery of their own language: many people that by the standards of a previous generation should know better, are no longer able to use their native tongue effectively, even for purposes for which it is pretty adequate. (You have only to look at the indeed alarming amount of on close reading meaningless verbiage in scientific articles, technical reports, government publications etc.) This phenomenon —known as "The New Illiteracy"— should discourage those believers in natural language programming that lack the technical insight needed to predict its failure. (End of remark.)

From one gut feeling I derive much consolation: I suspect that machines to be programmed in our native tongues —be it Dutch, English, American, French, German, or Swahili— are as damned difficult to make as they would be to use.

Plataanstraat 5 5671 AL NUENEN The Netherlands

prof.dr.Edsger W.Dijkstra Burroughs Research Fellow

---

transcribed by Tristram Brelstaff
revised Fri, 19 Nov 2010