Explorando desarrollo AI-first, guardrails de código y la arquitectura de la descartabilidad.
Cada compilador ve tu código como un árbol, pero tu editor te deja editar texto en bruto. Así es como se ve realmente la edición estructurada, por qué no se ha impuesto y cómo aprovechar sus beneficios sin cambiar de herramientas.
Cada lenguaje de programación tiene una gramática formal. Tu compiler la lee, construye un árbol de análisis y rechaza todo lo que no encaje. Tu editor ignora…
La programación literaria prometía que el código debía escribirse primero para humanos y segundo para máquinas. Cuatro décadas después, casi nadie escribe de esa manera. He aquí por qué la idea más elegante en la documentación de software no logró cambiar la forma en que trabajamos.
En 1984, Donald Knuth publicó un artículo que proponía una inversión radical. Los programas no deberían escribirse para compilers y anotarse para humanos.…
La mayoría de los equipos arreglan defectos y siguen adelante. Los mismos defectos vuelven. Así es como ejecutar análisis causal dentro de una inspección Fagan para dejar de escribir el mismo bug dos veces.
Todo equipo tiene ese defecto que sigue volviendo. Un off-by-one en la paginación. Una verificación de nulo faltante en el middleware de autenticación. Una…
Múltiples estudios en IBM, AT&T, HP y Microsoft confirman que la revisión informal de código detecta aproximadamente una cuarta parte de los defectos. Aquí está lo que los datos realmente dicen, por qué el número es tan bajo y cómo solucionarlo.
La revisión informal de código detecta entre el 15 y el 30 por ciento de los defectos presentes en el código que se revisa. Esa no es una opinión. Es un…
La mayoría de las checklists de revisión son listas copiadas y pegadas de buenas intenciones. Una checklist estructurada al estilo Fagan inspection se construye a partir de datos reales de defectos, está dirigida a tipos de artefactos específicos y se utiliza durante la preparación individual. Así es como se construye una que funciona.
Si tu equipo tiene una checklist para code review, hay una buena probabilidad de que viva en una página wiki que nadie abre. Probablemente dice cosas como…
Las inspecciones Fagan necesitan de cuatro a seis personas y dos horas para revisar 250 líneas. Un LLM puede reducir ese costo gestionando la preparación y el cumplimiento de checklist, pero no puede sustituir los roles humanos que encuentran los defectos más costosos.
Una inspección Fagan completa necesita un moderador, un lector, de dos a cuatro inspectores y el autor. El equipo dedica dos horas a revisar aproximadamente…
El proceso de revisión estructurado de Michael Fagan en IBM atrapaba casi todos los defectos antes de que llegaran al compilador. También consumía el 15-20 % del esfuerzo total del proyecto. Aquí está por qué desapareció el método de revisión más efectivo en la historia del software, y qué es lo que los equipos realmente extrañan.
En 1976, Michael Fagan publicó un artículo en el IBM Systems Journal que describía un proceso de revisión tan eficaz que se convirtió en el estándar de oro…
Incluso los ingenieros senior detectan solo una fracción de los defectos en revisiones no estructuradas. La investigación de Michael Fagan en IBM mostró por qué, y construyó un proceso de inspección estructurado para solucionarlo.
Dos ingenieros senior revisan el mismo pull request. Uno señala un null check faltante. El otro detecta una race condition en el cleanup path. Ninguno…
La revisión de código informal detecta el 15-30 % de defectos. Las Fagan inspections, un proceso estructurado de 50 años, reportan consistentemente tasas de eliminación del 60-90 %. Aquí se explica cómo funcionan, por qué los equipos las evitan y cómo ejecutar una versión ligera.
La mayoría de las code reviews detectan entre el 15 y el 30 por ciento de los defectos que deberían encontrar. Eso no es una suposición. IBM lo midió en los…
AutoVerus utiliza una red de agentes LLM para generar proofs de corrección de Verus para código Rust, automatizando más del 90% de las proof obligations mediante un bucle de generar-reparar-dischargar impulsado por el feedback del solver SMT.
La parte más difícil de la verificación formal nunca ha sido el verificador. Es escribir el proof. Dale a un ingeniero senior de Rust Verus, el verificador…