Métodos formales y el futuro de la programación
(blog.janestreet.com)- Los métodos formales son herramientas para demostrar que el software cumple las propiedades previstas, y la expansión de la programación con agentes está cambiando cómo se evalúan sus costos y beneficios
- Jane Street antes consideraba que, salvo algunos casos especiales, los métodos formales ofrecían poco valor frente a su costo, pero ahora está formando un equipo dedicado
- Verificar las 8,700 líneas de código C de seL4 tomó 25 años-persona, y se requirieron unas 23 líneas de prueba y medio día-persona de verificación por cada línea de código
- El código generado por agentes todavía difiere de la calidad necesaria para lanzarse a producción, y los métodos formales se vuelven importantes como medio para reducir el cuello de botella de verificación y dar retroalimentación fuerte a los agentes
- Jane Street cree que, como puede controlar profundamente su lenguaje y cuenta con una comunidad de programadores preparada, hay espacio para desarrollar OxCaml junto con técnicas orientadas a pruebas
Métodos formales y el futuro de la programación
- Jane Street ha dicho durante los últimos 25 años que no tenía interés en los métodos formales a nivel organizacional, pero ahora ya no mantiene esa postura
- Desde hace mucho ha valorado el poder de las herramientas para escribir mejor código y código más confiable, y considera a los sistemas de tipos como una forma ligera de método formal que ha dado grandes beneficios
- Salvo en casos especiales, especialmente la síntesis de hardware, había considerado que los métodos formales eran demasiado costosos para encajar en la mayoría del software
- seL4 fue un microkernel verificado formalmente y un logro importante, pero verificar sus 8,700 líneas de código C tomó 25 años-persona
- Se requirieron unas 23 líneas de prueba por cada línea de código, y alrededor de medio día-persona para verificar una sola línea
- En casos de alto riesgo y con especificaciones relativamente claras, como un microkernel crítico para la seguridad, este enfoque puede valer la pena
- No parecía adecuado para la mayor parte del software, ni tampoco para el software más importante de Jane Street
- La llegada de la programación con agentes cambió esa evaluación, y el escepticismo sobre el potencial de los métodos formales se transformó en expectativa
- Jane Street está formando un equipo de métodos formales y espera convertirlos en una herramienta de construcción de software tan ampliamente útil como los sistemas de tipos sofisticados
Por qué cambiaron de opinión
- La programación con agentes altera de varias formas la relación tradicional de costo-beneficio de los métodos formales
- Eso no significa que un agente pueda construir por sí solo pruebas arbitrariamente difíciles, pero los modelos ayudan mucho y permiten que más personas usen estas herramientas de forma productiva
- Como usar métodos formales ahora es más fácil que antes, vale la pena reconsiderar el cálculo histórico entre costo y beneficio
-
El cuello de botella de verificación se vuelve más importante
- Los modelos escriben código útil cada vez mejor, pero sigue habiendo una gran diferencia entre el código que generan y el código que realmente puede liberarse
- Los modelos son sorprendentemente buenos para cumplir el objetivo dado, pero no son lo bastante sólidos para mantener o mejorar la calidad del codebase durante el proceso
- El código hecho por agentes está mejorando, pero tiende a ser excesivamente complejo, con bugs extraños y muchos casos límite, y a no respetar los invariantes centrales del codebase
- Las personas todavía deben dedicar mucho tiempo a verificar si el código producido por agentes tiene la calidad suficiente
- Los métodos formales pueden reducir esta carga de verificación y hacer más eficiente el proceso de revisión
-
Los agentes mejoran con la retroalimentación
- Los agentes se benefician de la retroalimentación tanto cuando se entrenan con aprendizaje por refuerzo como cuando se usan para programar
- Los métodos formales pueden convertirse en una forma poderosa de retroalimentación para aumentar la capacidad de los agentes de resolver problemas difíciles
- Las pruebas también son muy valiosas, y pueden mejorar aún más con property-based testing y fuzzing
- Pero las pruebas por sí solas no bastan, y tienen límites inherentes para cubrir el espacio de estados que un programa puede recorrer
- En la experiencia de programación con OxCaml, los agentes se benefician mucho de las garantías universales que ofrece el sistema de tipos
- Si un sistema de tipos puede impedir data races, entonces puede eliminar las data races
- Si los tipos se diseñan bien para volver imposibles vulnerabilidades de cross-site scripting, pueden eliminarse de una manera que las pruebas simples difícilmente logran
- Los tipos alivian el cuello de botella de verificación y ofrecen mejor retroalimentación cuando se programa junto a agentes
- El uso de técnicas de prueba más potentes podría abrir espacio para mejoras adicionales
Por qué aquí
- Todo el mundo está pensando en lo que los agentes significan para el futuro de la programación, y también hay muchas startups que buscan combinar métodos formales con agentes
- Jane Street puede controlar profundamente el lenguaje que usa, así que puede ajustarlo para hacerlo más apto para técnicas orientadas a pruebas
- Hay varias direcciones posibles
- Se pueden integrar especificaciones modulares de propiedades en el sistema de tipos
- Se pueden agregar restricciones a nivel de tipos sobre elementos como ownership y mutability para facilitar ciertas pruebas
- Se pueden incorporar técnicas de prueba directamente en el lenguaje
-
Una comunidad de programadores preparada
- En Jane Street hay una comunidad de programadores preparada para adoptar este tipo de técnicas
- Para quienes trabajan con lenguajes de programación, lograr que una buena idea de programación se use en el trabajo real suele ser más difícil que inventarla
- En Jane Street es común que los usuarios se quejen de que funciones nuevas y poco familiares del sistema de tipos prometidas no llegan con suficiente rapidez
- Ya hay muchas personas con el trasfondo necesario para aprovechar estas técnicas, y también existe un interés arraigado por producir resultados correctos y software de alta calidad
- Una base de usuarios activa y con altas expectativas da libertad para intentar mejoras de corto plazo junto con una visión de largo plazo
- Las mejoras de corto plazo pueden tener impacto relativamente rápido
- La visión de largo plazo puede convertirse en una meta más ambiciosa alcanzable a lo largo de varios años
- Se puede aprender de los intentos de corto plazo mientras se construye hacia objetivos de largo plazo
-
Relación con herramientas externas
- No están ignorando el trabajo del mundo exterior, y ven con expectativa e inspiración el trabajo de varias comunidades de lenguajes de programación
- Entre las herramientas relacionadas están Lean, Dafny, Rocq, Agda e Iris
- Están buscando formas de integrar OxCaml con algunas herramientas para aprovechar la excelente infraestructura que ya existe
- También creen que hay ventajas únicas que solo pueden lograrse al trabajar simultáneamente con el lenguaje y con las técnicas de prueba
Invitación a unirse
- Jane Street está buscando personas relacionadas con métodos formales en London y New York
- Las entrevistas y la formación del equipo para esos puestos todavía están en una etapa inicial
- Hay muchísimo trabajo por hacer y están buscando personas para sumarse al equipo
Complemento
- Los modelos todavía necesitan ayuda y guía humana al tratar con pruebas complejas
- Los programadores humanos pueden tener ideas sobre por qué funciona un sistema y cómo demostrarlo a alto nivel
- La mayoría de los programadores no sabe cómo codificar una idea de prueba de una manera que satisfaga un sistema de pruebas específico
- Los modelos pueden automatizar gran parte del trabajo repetitivo y aportar experiencia en los detalles técnicos de escribir pruebas
- Escapes como
Obj.magicpueden permitir eludir restricciones a nivel de tipos - Si estas excepciones se rastrean y prohíben en la mayor parte del código, se puede lograr un estado muy cercano a las garantías universales
- Los métodos formales pueden hacer explícito por qué el uso de este tipo de escapes es realmente seguro
1 comentarios
Comentarios de Hacker News
Hace décadas trabajé en pruebas de corrección, y en ese entonces el sistema tenía más automatización de pruebas que muchos sistemas posteriores.
La parte fácil la resolvía el simplificador Oppen-Nelson, el primer solver SAT, y la parte difícil la llevaba el demostrador Boyer-Moore usando heurísticas y lemas previos. El trabajo difícil para la persona era dejar que el demostrador lo intentara y luego proponer lemas que pudieran usarse en pruebas posteriores.
Los sistemas posteriores parecieron reducir la automatización, y creo que la razón por la que los métodos formales se desviaron fue porque se enamoraron demasiado del formalismo por encima de la práctica. Desde la perspectiva de alguien que quería código sin bugs en proyectos comerciales, sentía que los proyectos académicos caían en un sesgo de matemático que prefería notación compacta para papers y análisis con pocos casos.
En la práctica se necesita mucho trabajo automatizado de fuerza bruta y se necesita menos intuición. Gente muy lista siguió creando nuevas lógicas como lógica modal y lógica temporal para evitar la verbosidad de las pruebas en papel y lápiz, pero no ayudó mucho. La verdad básica de este campo es que la mayoría de los teoremas son bastante corrientes.
Como dice la gente de Jane Street, poder controlar el lenguaje es una gran ventaja. Las afirmaciones de verificación deberían integrarse dentro del lenguaje de programación, y si quedan metidas en comentarios, otra sintaxis o archivos separados, aumenta el trabajo innecesario. Se ve bien que Jane Street esté empujando en esa dirección.
Hice este trabajo demasiado temprano, hace más de 40 años, y en ese momento construir teoría de números desde cero con el demostrador Boyer-Moore tomaba unos 45 minutos de cómputo, pero ahora tarda menos de 1 segundo.
https://archive.org/details/manualzilla-id-5928072/page/n3/m...
La lógica ocupa en ciencias de la computación e ingeniería de software un lugar parecido al del cálculo en física, ingeniería mecánica e ingeniería civil. Cosas como LTL o la más reciente lógica de separación fueron avances enormes.
La bastante popular TLA+ es prueba de ello, y el model checking es muy práctico. Lo interesante ahora es que métodos formales más pesados, en particular la demostración de teoremas, podrían volverse lo bastante baratos como para usarse incluso en software de sistemas general.
Escribir una especificación formal para una función y luego sintetizarla con un híbrido de SAT/SMT, demostradores de teoremas y LLM, y recibir una prueba de corrección, podría convertirse pronto en lo estándar.
On the Unusual Effectiveness of Logic in Computer Science: https://www.cs.rice.edu/~vardi/papers/aaas99.jsl.pdf
From Philosophical to Industrial Logics: https://www.cs.rice.edu/~vardi/papers/icla09.pdf
Lo preocupante es que aparezcan matemáticas difíciles de descifrar y que un pequeño grupo de creyentes las resguarde. Distintas notaciones crípticas no serían compatibles entre sí, y entender una podría no ayudar mucho a entender otra. La mayoría terminará escribiendo solo frases en inglés que no pueden verificarse correctamente.
Peor aún, podríamos poner a la máquina a formalizar sus propias oraciones y luego participar en un teatro de verificación sin entender ese formalismo ni las pruebas, para después fingir sorpresa cuando todo explote.
Se está avanzando lentamente en integrar este tipo de capacidades en las partes que el sistema de tipos no puede manejar rápido, así que me interesa la perspectiva de quienes ya recorrieron ese camino.
Bien. En los últimos meses he estado usando tipos expresivos en Scala 3 para mover más y más pruebas en tiempo de compilación dentro de los tipos. No uso macros, aunque algunas sí podrían servir.
Este enfoque no solo parece ayudar a reducir el problema de que se propaguen las pruebas tipo agente, sino que también parece evitar que el agente caiga en formas de trabajo de baja calidad. En particular, evita la acumulación de sustantivos, donde el agente quiere crear un nuevo tipo nominal para todo, incluso cuando razonablemente debería generalizar.
Creo que lo que acelerará la programación de agentes de buena calidad son herramientas parecidas a los métodos formales, incluyendo lenguajes con sistemas de tipos fuertes.
Aquí, por tipos expresivos me refiero a técnicas que no querrías meter en una base de código general si el equipo no está ya acostumbrado a la programación a nivel de tipos. Es decir, debe ser un equipo para el que los tipos de orden superior y las funciones de tipo no sean rarezas, sino bloques básicos.
En conocimiento, los agentes suelen ser mejores que la mayoría de los desarrolladores para las “matemáticas”, y muchas veces incluso mejores que desarrolladores empapados de teoría de categorías. Además, si asumimos que tienen paciencia “infinita” para la conversación, también enseñan bastante bien.
Personalmente, le pedí a Codex que convirtiera algunas pruebas de hobby al estilo Lean, y fue muy fácil. No diría que es 100% “correcto”, y para comprobarlo con más rigor tendría que aprender más Lean 4, pero en esencia parece revisar también las trampas clásicas de las demostraciones. Me entusiasma mucho el futuro de los métodos formales.
Parece que la idea es que, como la Gen AI genera muchísimo código, traslademos el valor humano hacia la verificación. A veces me pongo a pensar qué es realmente programar
Para quienes no tenemos el inglés como lengua materna, aprender a programar ya es de por sí un gran desafío. Para entender documentación en inglés no traducida, hay que depender de la traducción automática, y el material en mi idioma está atrasado unos 5 o 6 años
Ahora que es imposible hacer code review de decenas de miles de líneas de código hechas por AI, parece que están surgiendo debates sobre establecer reglas absolutas, como pruebas matemáticas. Al leer esto pensé en el borrow checker de Rust. De hecho, cuando usas Rust algunas veces, la gente muchas veces termina desarrollando el mal hábito de hacer trucos para esquivar el borrow checker
Cuando la rigurosidad matemática es excesiva, la gente busca rodeos. Los programadores con poca formación, como yo, somos especialmente propensos a eso
Siento que este tipo de intento al final llevará a escribir código solo para ciertas respuestas formalizadas. Y si todo se estandariza así, no estoy seguro de que pueda responder a las necesidades humanas
Estos intentos de programación defensiva me parecen bien, pero, usando una expresión mía, yo quiero hacer programación agresiva. Es una forma de trabajar en la que se asumen riesgos, pero se corrige y se despliega rápido, confiando en que con el tiempo será lo bastante buena
Claro, en industrias ya establecidas como Jane Street, donde la precisión es importante y el alcance del trabajo está bien definido, el enfoque del artículo sí encaja. Porque hay suficientes datos como para modelar adecuadamente las demandas del mercado
Pero para un perdedor social como yo, que va moviéndose en busca de una mina de oro para ganar dinero, esta metodología parece un lujo. Sé que los negocios existentes con modelado maduro necesitan que profesionales especializados y con alta formación sigan optimizándolos, y que en la práctica es imposible seguirle el ritmo a esa demanda. Por eso busco lugares donde el modelado no está estructurado, aunque tampoco sé si este enfoque serviría ahí
Ahí no existe eso de “ya se arreglará”. Para cuando entiendas qué salió mal, puede que ya hayas perdido miles de millones
Por eso el enfoque agresivo puede funcionar en áreas no centrales
Además, de hecho ya se usan enfoques defensivos en muchos lados. Python, Java y otros tienen garbage collector, y en cierto sentido eso verifica que el código se ejecute como se pretendía
Me preguntaba cuándo empezaríamos a ver verificación formal, y es natural pasar de preocuparse por detalles de implementación a describir los problemas de forma científica y matemática
Por culpa de la Gen AI, el costo de la programación defensiva bajó muchísimo, y el costo de la verificación humana subió muchísimo. En cambio, los métodos formales abaratan la verificación, pero tienen un gran sobrecosto de implementación: escribir especificaciones, tipos y pruebas, y forzar la implementación a entrar en un marco rígido
Pero la Gen AI puede automatizar ese trabajo pesado. Son la pareja perfecta
Requiere algo de esfuerzo, pero eliminar esa carga continua de traducción te va a ayudar muchísimo
Dicho eso, no entiendo muy bien qué relación tiene este punto con llamarte a ti mismo “perdedor social” o con no seguir este tipo de prácticas en tu carrera
Últimamente he estado jugando con ideas relacionadas, y lo que me sorprendió fue lo bien que los modelos de frontera, en especial ChatGPT-5.5, completan ciertas pruebas manuales en Roqc, antes Coq, el asistente de pruebas
Las pruebas no siempre quedan bonitas, pero ChatGPT muchas veces logra en unos minutos y tras 10 a 100 iteraciones algo que a mí me llevaría bastante más tiempo, incluso teniendo experiencia limitada, pero no nula, con asistentes de pruebas y bastante experiencia en el dominio de los lemas auxiliares que se están demostrando
En el contexto de este breve texto, esto es interesante porque sacude los supuestos básicos sobre cómo funcionan ciertas herramientas de métodos formales. Frama-C, Ada/SPARK y otras se enfocan en generar obligaciones de prueba que herramientas como CVC5 o Z3 puedan resolver automáticamente, y si eso falla, se pasa a la alternativa bastante dolorosa de hacer la prueba manualmente en Roqc
El flujo habitual es detectar que cierta obligación es “difícil”, o sea, que no se resuelve automáticamente, y entonces reestructurar el conjunto de lemas auxiliares y aserciones visibles en el punto del código donde se genera la obligación para volverla “fácil”, o incluso cambiar el código
Eso tiene sentido en un mundo donde una prueba en Roqc cuesta el doble. Es difícil de escribir para una persona, y además tiene mucha variabilidad de mantenimiento cuando cambia el código o cambian las pruebas de alrededor
Pero si una prueba en Roqc pasa a ser una “resolución automática con AI en el loop”, esa diferencia de costos desaparece. Entonces se podría escribir pruebas como se escribe código, priorizando ante todo la claridad legible para humanos, y dejando mucho después la optimización para el compilador o el demostrador. Todavía no termino de procesar todas las implicaciones, pero me parece bastante interesante
Nunca he trabajado con pruebas, pero sí me ha pasado a veces que, cuando le digo a la AI “después del cambio este test falló”, en vez de corregir el código para que pase tanto el test anterior que yo quería como el nuevo test, termina cambiando el propio test
Tengo muchas ganas de ver qué viene después
Cada vez que leo sobre especificaciones formales, me parece “escribir las mismas pruebas de otra manera” y, peor aún, “escribir la misma implementación de otra manera”.
Es cierto que escribirlo dos veces puede ayudar a detectar errores, pero si una especificación formal también puede tener exactamente los mismos bugs que las pruebas o la implementación, no me queda claro qué tiene de especial.
El problema de fondo es que, para demostrar formalmente que un programa hace algo, hay que definir ese “algo” de manera muy concreta. Entonces, en la práctica, termina pareciendo que vuelves a escribir las pruebas o la implementación.
Llevo años mirando este tema de forma intermitente y sigo con la sensación de que me estoy perdiendo algo, pero no sé qué es. ¿Alguien podría explicarlo?
El defecto de las pruebas es que solo puedes probar los comportamientos que se te ocurrió que podrían ser un problema. Para corregir por adelantado comportamientos que ni siquiera sabías que podían salir mal, necesitas herramientas más inusuales en la caja. El fuzz testing es un inicio en esa dirección, y la verificación formal es otro.
Por supuesto, la calidad de estas herramientas depende de qué tan bien escribas un modelo formal y abarcador que permita el comportamiento deseado y prohíba el no deseado, y en muchas áreas seguimos estando sorprendentemente lejos de ese punto.
Por ejemplo, en una prueba unitaria puedes escribir “foo('abc') devuelve una cadena sin espacios al final”.
Pero con técnicas formales puedes demostrar “para cualquier entrada x, foo(x) devuelve una cadena sin espacios al final”.
Es un ejemplo trivial, pero también puedes imaginar algo más complejo, como “para cualquier programa P, compile(P) se comporta igual que P”.
Claro, hay que definir qué significa exactamente “se comporta igual”.
Defines propiedades del diseño y la herramienta prueba el diseño de muchas maneras distintas para verificar si puede violar esas propiedades.
Por ejemplo, si fuera un sistema que controla semáforos, podrías especificar la propiedad de que carriles que se cruzan no pueden tener luz verde al mismo tiempo, ni ambos dentro de cierto intervalo de tiempo.
La herramienta puede verificar esto mediante búsqueda exhaustiva y mostrar una traza del código que viola la propiedad.
Un sistema de tipos demostrado estáticamente permite comprobar de antemano que cada componente encaje con todos los demás. No solo garantiza “esta prueba pasa”, sino que, al combinarlas, asegura “todas estas pruebas forman un todo razonable y coherente”, y evita que un modelo incoherente se implemente en el código.
Es parecido a tomar el requisito de
matchen Rust de cubrir por completo todas las ramas posibles y escalarlo al tamaño de toda una base de código.Es cierto que no puede salvarte si introduces errores fundamentales de lógica o de teoría. Pero podría sorprenderte lo mucho más sólido que resulta, por ejemplo, que combinar el sistema de tipos de Haskell, pruebas funcionales ad hoc y property testing. Todo eso en conjunto ya parece un sistema fuerte, pero la criptografía demostrada formalmente está en un nivel mucho más alto.
Esto es especialmente valioso en escenarios de concurrencia, distribución y múltiples hilos. Las race conditions y los deadlocks son muy difíciles de probar y razonar, y lo mismo pasa con preguntas como “¿pueden A, B y C ocurrir en el orden A, C, B?”.
Creo que la madurez de este campo irá más o menos así. Primero, los LLM van a acelerar muchísimo el aprendizaje y uso de técnicas formales, aunque al principio se queden en una especie de verificación posterior de “hacerlo una segunda vez”.
Segundo, avanzaremos hacia automatizaciones donde el LLM revise “¿cambió el código de implementación de una manera que parece romper el modelo?”. Seguirá sin ser algo determinista, pero probablemente sea mucho mejor que obligar a una persona a revisar algo que solo cambia de vez en cuando.
Tercero, el verdadero salto estaría en llevar al siguiente nivel las herramientas de “escribe solo la especificación formal y genera la implementación”. Ya existen varios proyectos de generación de código de este tipo, pero la mayoría todavía no están completamente maduros para el nivel que quieren las empresas. ¿Y si las herramientas basadas en LLM pudieran acelerar ese trabajo manual de 1 a 2 años necesario para adaptar uno de ellos a tus necesidades?
También vale la pena ver el artículo anterior de Kleppmann https://martin.kleppmann.com/2025/12/08/ai-formal-verificati..., y obviamente conviene evaluar si lo que puedas meter en el sistema de tipos o en un linter debería ir ahí.
Ojalá aparezcan formas más cómodas de usar esto. Entre las herramientas mencionadas en el artículo, dafny e iris parecen las más cercanas a un uso industrial. También sé que Amazon S3 tiene historial de haber usado TLA internamente.
Pero todavía no creo haber visto el TypeScript de este campo: algo que entre de forma natural en las herramientas existentes, funcione como una abstracción sin costo y que la gente de verdad prefiera por encima de la forma anterior de trabajar.
Incluso usar linters personalizados sigue siendo bastante desagradable. golangci-lint es una base de código dolorosa, no he usado semgrep pero su motor de reglas me parecía intimidante. Tampoco he llegado a usar todavía una API de AST que realmente me guste.
Este tipo de elogios al razonamiento deductivo, es decir, a los “métodos formales”, siempre omiten su limitación fundamental: qué tan bien encajan los axiomas y las definiciones con el dominio objetivo
Es como decir: “En teoría, no hay diferencia entre la teoría y la práctica. En la práctica…”. Se supone que Jane Street mantendrá una gran base de código donde el mapeo es 1:1, porque el propósito del código es implementar algoritmos deterministas. Muchos desarrolladores trabajan en áreas así, pero millones no. La mayoría de las UI, gran parte del trabajo exploratorio, etc., no son así
En paralelo a los métodos formales, también hay una corriente que intenta definir los criterios de aceptación con alta resolución, aunque no de forma lógico-matemática. Esa corriente al menos lidia con el problema del mapeo, pero no lo resuelve en la mayoría de los lugares donde el mapa no es el territorio
La página de resultados de búsqueda de Google tiene un framework interno de optimización extremadamente evolucionado, pero ¿de verdad llegó al óptimo? ¿Podría un prototipo armado a las apuradas para capturar una idea borrosa haber mostrado algo mejor? Estas preguntas se responden mejor mirando no dentro del sistema, sino afuera, hacia aquello a lo que el sistema sirve
Los circuitos lógicos, los componentes de CPU con mucha verificación formal, kernels, protocolos, parsers, compiladores, criptografía, frameworks de seguridad, primitivas de concurrencia, etc., se benefician enormemente de la verificación
Si quieres aprender más, el texto de Hillel Wayne es un buen punto de partida: https://www.hillelwayne.com/formally-specifying-uis/
Y en algunos casos, aunque el resultado no esté bien definido, aún puedes aprender, así que no es solo un problema de sentarse a pensar qué tendría sentido
Desde la perspectiva de alguien con algo de interés en el diseño e implementación de lenguajes de programación, esta frase me pareció realmente interesante. “Para la mayoría de las personas que trabajan con lenguajes de programación, la parte fácil es tener ideas nuevas y mejores para hacer que programar sea mejor. La parte difícil es convencer a alguien de usar esas ideas en trabajo real”
Estoy totalmente de acuerdo. Incluso si hay beneficios, hay un límite a la cantidad de extrañeza que puedes meter en un lenguaje nuevo
Pero los agentes de AI probablemente no sentirán una gran resistencia ante ideas radicalmente nuevas en el diseño de lenguajes de programación. Llevo un tiempo pensando en cómo podría evolucionar el diseño de lenguajes de programación después de la AI agentica
Será muy interesante ver qué ideas nuevas se podrían crear para mejorar los lenguajes de programación cuando haya mucho menos de qué preocuparse por la adopción
https://steveklabnik.com/writing/the-language-strangeness-bu...
Estoy trabajando en aplicar métodos formales al área de pruebas de seguridad de aplicaciones, y creo que el mismo enfoque puede aplicarse también a la verificación de lógica de negocio
Para esto estamos usando taint analysis. Es un enfoque de métodos formales bastante bien establecido, pero todavía no se ha aplicado ampliamente en campo debido a la complejidad del flujo de datos en bases de código reales
Extender los métodos formales más allá del pattern matching de AST y la simple verificación de tipos es un trabajo realmente difícil. Nos tomó años de I+D llegar al punto en que, con taint analysis, podemos rastrear en pocos minutos el flujo de datos interprocedimental en bases de código reales y encontrar vulnerabilidades profundamente ocultas
Si te interesa, puedes ver el proyecto: https://github.com/seqra/opentaint
Hace unos 18 meses me obsesioné con usar tipos junto con LLM, y me puse serio con
lean4hace unos 6–8 meses. Ahora ni siquiera consideraría usar asistencia de AI en trabajo de software sin una base de pruebasCICcon FFI práctico para C/C++, y por tanto conectable con prácticamente todoProhibimos todo, desde JSON hasta Python, y hasta reescribimos
nixpara que tuviera compilador. Casi todo lo que usamos no solo pasa property testing y múltiples fuzz tests hasta el límite, sino que además tiene pruebas enlean4que impulsan property tests al menos mediante enlazado.olean. Si tenemos margen, incluso demostramos completitud de dominio completo y también probamos esas propiedadesTodo lo rápido se genera en
lean4, así que nos saltamos el debate C++/Rust. Tiene ventajas cuando un bug de C++ en realidad resulta ser un bug en códigolean4, pero podría ir en cualquier direcciónEs un cambio grande, y no culpo a la gente escéptica que dice “¿prohibir JSON y Python?”. Pero nosotros hemos inspeccionado millones de líneas de esta manera, y AI + sistema formal es un salto mucho mayor que pasar de no tener AI a tener AI y Python. Según nuestra experiencia, esto último no avanza de forma monótona, pero lo primero casi siempre sí
También se pueden hacer cosas bastante atrevidas. Esta es una prueba formal de cálculo tensorial poliedral del tipo que modelan cosas como ISL y CuTe, y con eso puedes hacer swizzling y tiling en dispositivo con
mdspande C++23 y además demostrar que es correcto. Aunque este ejemplo no muestra muy bien un argumento tipo L'Hopital sobre cobertura: https://github.com/b7r6/mdspan-cuteEl resultado es realmente rápido, y rápido desde el primer intento
https://straylight.software/assets/lambda-hierarchy.svg