Ideas & Insights

Explorando desarrollo AI-first, guardrails de código y la arquitectura de la descartabilidad.

cleanroom-correctnessllmformal-proofsautomation

Los LLM no pueden demostrar que tu código es correcto, pero pueden escribir el código repetitivo que lo logra

La verificación Cleanroom requiere generar y descargar obligaciones de prueba. Así es como los LLM automatizan la anotación y la generación de condiciones de verificación (VC) para que puedas centrarte en las pruebas realmente difíciles.

La ingeniería de software Cleanroom exige que demuestres que tu código es correcto antes de compilarlo. Suena noble hasta que pasas tres horas escribiendo…
cleanroom-correctnessprocessefficiencypragmatism

Cleanroom Entrega 0.1 Defectos por KLOC. No Necesitas la Religión Completa para Llegar Ahí.

La ingeniería de software Cleanroom reduce las tasas de defectos 100×, pero la adopción completa requiere equipos de prueba separados y pruebas formales. Aquí tienes un subconjunto pragmático que captura la mayor parte del beneficio sin el overhead.

La ingeniería de software Cleanroom entrega 0.1 defectos por mil líneas de código. El promedio de la industria es de 10 a 50. El problema es que Cleanroom…
cleanroom-correctnesszero-defectssoftware-historyprocess

El Zero-Defect Process de IBM entregó 0.1 bugs por KLOC. La industria lo abandonó de todos modos.

El Cleanroom engineering de IBM alcanzó tasas de defectos 100 veces mejores que el promedio de la industria, y luego se desvaneció en la oscuridad. La desaparición no tuvo nada que ver con si funcionaba.

El Cleanroom software engineering process de IBM entregó 0.1 defectos por mil líneas de código. El promedio de la industria en ese momento estaba entre 10 y…
cleanroom-correctnesszero-defectsverificationcase-study

¿Alguien realmente verificó 10.000 líneas con cero defectos? IBM lo hizo, y la metodología es más extraña que el resultado.

Cleanroom software engineering prometió incrementos zero-defect mediante mathematical verification en lugar de debugging. Analizamos los datos reales del proyecto de IBM para ver si la afirmación se sostuvo.

El promedio de la industria del software en la década de 1980 era de 30 a 60 defectos por mil líneas de código. El equipo Cleanroom de IBM entregó un…
cleanroom-correctnessibmzero-defectssoftware-quality

IBM entregó software con 0,1 defectos por KLOC prohibiendo a los desarrolladores ejecutar su propio código

El proceso de ingeniería Cleanroom de IBM logró tasas de defectos 100 veces mejores que el promedio de la industria al prevenir bugs en lugar de encontrarlos. Así funcionaba, por qué casi nadie lo usa y qué puedes adoptar de él hoy.

IBM entregó un sistema de control de satélites de la NASA con 0,1 defectos por mil líneas de código. El promedio de la industria en ese momento estaba entre 10…
literate-programmingci-cdweave-tangleautomation

Tu programa literario está roto hasta que CI pueda hacer tangle sin ti

La programación literaria promete una única fuente de verdad, pero los pasos manuales de weave y tangle rompen la pipeline de CI/CD. Así es como automatizar la extracción y generación de documentación para que tus archivos Markdown sean canónicos.

Si tu pipeline de construcción no puede ejecutarse sin que abras una terminal y escribas , no tienes un programa literario. Tienes un diario con un compiler…
literate-programmingdocumentationtestingsingle-source-of-truth

Dejé de copiar código en la documentación manteniendo tests, código y prosa en un solo archivo Markdown

La programación literaria mantiene la documentación, los tests y la implementación sincronizados al convertir un archivo Markdown en la única fuente de verdad. Así es como implementarlo en treinta líneas de Python.

Tus docs, tests y código son tres archivos contando la misma historia mal. Actualizas la firma de la función en el source. Olvidas el ejemplo del README. Una…
literate-programmingllmdocumentationai-engineering

Tu Thread con Claude Ya Es Documentación. Solo Muere en Doce Horas.

Las conversaciones con LLM contienen intención, alternativas rechazadas y código funcional. Eso es exactamente lo que la documentación debería ser. Aquí está cómo convertir chat efímero en documentación durable y buscable sin perder la narrativa.

Pasaste cuarenta y cinco minutos con Claude diseñando un circuito de reintento. Explicaste los modos de falla, rechazaste el backoff exponencial porque oculta…