Buen artículo. Desde mi experiencia previa con verificación de programas, Rust parece el lenguaje moderno más útil para aplicar técnicas formales.
Las reglas de Rust eliminan muchos casos difíciles de formalizar. El gran problema que queda es el análisis de interbloqueos desde la perspectiva de los hilos y desde la perspectiva de Rc/préstamos; ambas son, en cierta medida, equivalentes. Si Rust tuviera análisis estático de interbloqueos, creo que también serían posibles los punteros de desreferenciación seguros, y si se pudiera demostrar que todas las llamadas borrow/upgrade no fallan, se podría eliminar la mayoría del conteo de referencias. Entonces, en los casos posibles, la mutabilidad interna también saldría gratis.
El gran problema de los demostradores de teoremas es que, como los construyen personas a las que les gusta demostrar teoremas, caen en el formalismo y su sentido de UI queda desalineado con el de los programadores. La mayoría de las obligaciones de prueba se pueden manejar con un solucionador SAT, pero los problemas difíciles requieren herramientas más pesadas. Coq es demasiado manual, y el autor considera que ACL2 es demasiado funcional. El aprendizaje automático puede ayudar a orientar a los demostradores de teoremas. Es difícil encargarle la prueba en sí, pero parece posible inferir planes de prueba en código donde el flujo de control y el uso de datos son, en general, parecidos.
F* se acerca a ese lenguaje mítico que demuestra automáticamente. Usa un solucionador SMT, más potente que SAT, y si la resolución automática falla, también permite pruebas manuales.
Las rutinas criptográficas de Firefox y Wireguard no están escritas en Rust, sino en F*, más precisamente en Low*, un DSL de bajo nivel incorporado en F*, y están completamente verificadas. https://project-everest.github.io/ https://mitls.org/
Estoy de acuerdo, pero creo que Lean, gracias a sus ricas capacidades de metaprogramación, está avanzando mucho en la experiencia de usuario de la verificación interactiva de teoremas.
El problema al aplicar estas herramientas a la verificación de lenguajes externos como Rust es que las pruebas no se escriben en el lenguaje objetivo, por lo que el desarrollador tiene que aprender dos lenguajes. A partir de mi experiencia escribiendo Creusot, del trabajo en Verus y Aeneas, y de la experiencia en el laboratorio de Why3, he estado pensando en cómo se vería un “Rust consciente de la verificación”. Si se creara un lenguaje así desde el principio, su facilidad de verificación podría mejorar por etapas incluso respecto de Rust, y creo que sería especialmente efectivo en las partes difíciles de las pruebas.
Creo que la familia Coq/Agda/Lean probablemente será la ganadora en el campo de las pruebas. La interacción es un modelo bastante bueno como ciclo de retroalimentación, y ya existen sistemas reales que funcionan.
Lo que más echo de menos como función integrada es algo equivalente a “ejecuta quickcheck sobre mi prueba”. Cuando tienes código e intentas demostrar una propiedad que no es verdadera, es fácil arrancarse los pelos sin entender por qué la prueba no sale. Si en medio de una prueba se llega a un estado sin sentido, sería bueno que un comando como “genera un contraejemplo aquí” devolviera un contraejemplo. Las pruebas dependen mucho del camino seguido y, en general, no son fáciles, pero estas herramientas parecen estar muy cerca de la grandeza. El proceso de intentar demostrar código también debería reflejar la posibilidad de que ese código tenga bugs.
La idea de que el aprendizaje automático guíe a los demostradores de teoremas es interesante. Si el sistema de aprendizaje automático acierta, guía hacia una prueba válida y se gana mucho; si se equivoca, no se pierde demasiado.
El demostrador no deriva una prueba incorrecta; simplemente no logra derivar una prueba válida. Creo que no hay muchas aplicaciones de aprendizaje automático con esa propiedad.
No soy especialista en verificación formal, pero no creo que los locks en el sentido tradicional ayuden mucho. Ningún compilador ofrece algo realmente útil sobre locks; simplemente hay que aceptar el riesgo y vivir con él.
En realidad, en Rust los locks y el conteo de referencias son estructuras en tiempo de ejecución. Arc rompe bastante el modelo RAII de Rust, hasta el punto de que hubo que eliminar los scoped threads cuyos destructores debían ejecutarse antes de que terminara el scope. El conteo global de referencias tiene problemas de ciclos y fugas, y vuelve a ser un problema global. Probablemente sea difícil eliminarlo por completo, pero creo que es mejor encerrarlo en scopes estilo arena. Para los locks parecen necesarias estructuras de datos asimétricas, como los canales. En Go, los canales se dividen en emisor y receptor, y en la goroutine emisora se puede poner defer close(ch); incluso si hay un panic, se garantiza que se ejecutará cuando termine el resto del hilo. No tiene que ser necesariamente un canal, pero separar los roles de lectura-escritura/productor-consumidor hace que el razonamiento sea mucho más fácil y también parece ayudar al análisis formal.
Me gusta que haya empezado con una cita del artículo de Hoare de alrededor de 1973 y que ahora ya haya llegado hasta un segundo texto. Originalmente dejé un comentario largo en el hilo de HN del artículo de boat, diciendo que inclinar esa cita hacia una perspectiva centrada en Rust es comprensible dado el trasfondo de boat, pero que reduce artificialmente el alcance de la crítica de Hoare
Ahora Grayson tomó ese fragmento estrecho como punto de partida para discutir algunas áreas interesantes y puntos de diseño de Rust. Sigo pensando que mi comentario era correcto, pero la discusión que surgió del texto de Grayson fue suficiente para compensar mis objeciones técnicas al texto que sirvió de punto de partida
Para mediados de los 90, más o menos, el propio Hoare ya se había dado cuenta de que quizá había algo mal en los fundamentos del enfoque centrado en la solidez de los años 70: http://users.csc.calpoly.edu/~gfisher/classes/509/handouts/h...
Desde entonces, con la aparición de técnicas no sólidas más avanzadas que las pruebas simples, creo que los métodos no sólidos terminaron adelantándose a los métodos sólidos
1973 fue hace 50 años, toda una vida profesional. Hoare estuvo realmente cerca
Identificó el problema y, visto en retrospectiva, la solución de imponer compartición XOR mutabilidad mediante el sistema de tipos parece un pequeño paso. Si en ese momento se hubiera descubierto que ese pequeño paso era la solución, se habría evitado una enorme cantidad de sufrimiento durante 50 años
Lo que escribí originalmente sobre la cita que hizo boat del artículo de Hoare fue esto. Después de la primera cita de Hoare y una breve introducción, el autor dice: “cuando Tony Hoare dijo que las referencias son como saltos, estaba tratando el problema del estado mutable y con alias”. Como withoutboats es un desarrollador conocido de Rust, esta interpretación no sorprende
Pero no me parece que la cita en sí refuerce esa perspectiva. Se puede ver como un intento de tomar el lamento más general de Hoare sobre la existencia semántica misma de las referencias y aplicarlo al modelo de estado mutable sin alias de Rust para esquivar el problema. Sin embargo, eso se parece más a arreglar un fragmento estrecho de un problema mayor y decir que todo el problema desapareció. Las partes omitidas, en especial el comienzo de la sección “Variables” y el ejemplo de ALGOL 68, se inclinan mucho más hacia la idea de que Hoare criticaba no solo el estado mutable, sino el propio concepto semántico de referencia. Reconozco el intento de Rust de domesticar una parte del problema, pero no creo que ningún lenguaje lo haya “arreglado”
No entiendo muy bien por qué este texto recibe tantos elogios. Siento que despacha varias áreas del análisis de programas en un solo párrafo. Me gusta Graydon y respeto su perspectiva, pero este párrafo está demasiado simplificado
La explicación de que los lenguajes con GC no se molestaron en ofrecer un soporte fuerte para el razonamiento local es un hombre de paja. Hubo lenguajes como Pony, que usan GC y aun así incorporan regiones en el sistema de tipos. Además, existen campos completos como el análisis de punteros y el análisis de escape, que infieren unicidad y determinan si dos referencias pueden ser alias. El núcleo del tipado estático también consiste en dividir el heap en partes que no se aliasan entre sí mediante la técnica de clases y campos. No estamos hablando de JavaScript, y no deberíamos fingir que Java/C#/Scala y muchísimos lenguajes con GC carecen de razonamiento local sobre el estado mutable
En el caso general, esto no puede hacerse automáticamente de forma completa y, en la práctica, se necesita algo bastante parecido a la lógica de separación. La semántica del borrow checker de Rust también puede verse como una especie de lógica de separación simplificada
Las clases y los campos no ofrecen razonamiento local completo sobre el estado mutable, porque una clase/objeto A puede llegar a depender del estado mutable de una clase/objeto B. La herencia de clases al estilo Java añade por sí sola aún más complejidad a medida que el programa evoluciona con el tiempo
Graydon no dijo que el GC haga imposible un razonamiento local fuerte. Lo que dice es que, por la razón que sea, la mayoría de los diseñadores de lenguajes tomaron decisiones opuestas a ese objetivo, y eso parece claramente cierto
Claro que hay contraejemplos, pero si miramos lenguajes de propósito general con GC y de uso masivo como Java, C# y Python, la afirmación es correcta. Es posible interpretar que la idea original de la orientación a objetos se parecía más al modelo de actores actual, y que pretendía modificar estructuras de datos con dueño únicamente mediante paso de mensajes. Pero las implementaciones reales de la orientación a objetos casi no se acercan a ese objetivo. Java no impide guardar referencias mutables al mismo objeto en varios objetos. Este artículo lo explica mejor: https://without.boats/blog/references-are-like-jumps/
Como quiz sencillo, ¿qué imprime este código? void myMethod(final Map map) { map.remove("key"); int oldSize = map.size(); map.put("key", "val"); int newSize = map.size(); System.out.println(newSize - oldSize); }
Edición: leí mal la doble negación. Incluso al releerlo, todavía me resulta confuso. ¿Quiere decir que Java, a diferencia de JavaScript, sí tiene razonamiento local?
Por lo general me gustan los textos de Graydon, pero este, como muchos artículos sobre técnicas formales, puede dar una impresión equivocada a lectores que no conocen el campo. Es parecido a decir que el método para convertir plomo en oro mejoró en una escala de un dígito, sin decir que todavía faltan 29 órdenes de magnitud para que sea práctico y costo-efectivo.
¿Que no tener aliasing facilita mucho la verificación formal? Sí. ¿Que por eso se puedan verificar programas reales de forma práctica y costo-efectiva? Para nada. Hay programas, circuitos y componentes que se verifican formalmente todos los días, pero son más bien excepciones, relativamente muy pequeños y construidos de una manera especialmente cuidadosa. Las propiedades que ayudan al razonamiento local son importantes, pero no cambian de forma sustancial cómo garantizar de manera sólida la corrección del software mainstream.
Incluso los programas en un lenguaje lejos de ser Turing completo —sin heap, sin punteros, sin enteros, solo variables booleanas y con bucles que no pueden ejecutarse más de dos veces— no se pueden verificar en la práctica porque se reducen a TQBF. Para ciertas propiedades, por ejemplo la seguridad de memoria, sí puede ser posible, pero no alcanza para lo que necesita el software. En los años 70 a 90 existía la esperanza de que, aunque la complejidad del peor caso fuera intratable, las garantías locales y la estructura del lenguaje nos alejarían del peor caso; después se demostró que no era así. La esperanza de que los programas que la gente realmente escribe estén lo suficientemente lejos del peor caso como para que surjan buenas heurísticas tampoco parece sostenerse ya.
Hay una charla relacionada sobre esto: https://pron.github.io/posts/correctness-and-complexity
El resultado clave es que la mayoría de las propiedades interesantes que uno querría verificar no son composicionales. Aunque se demuestre una propiedad para cada componente P1...Pn, el costo de demostrar esa propiedad para P1 ○ ... ○ Pn no solo crece de forma superpolinómica respecto de n, sino también respecto del tamaño de cada componente. Es decir, es tan difícil como si no se hubiera dividido, y la corrección no se descompone. Por eso “se pueden verificar bastantes cosas” y “lo verificable es una gota en el océano” pueden ser ambas afirmaciones verdaderas, y en las discusiones sobre técnicas formales a menudo se omite esa brecha.
Llevo más de 6 años repitiendo el mismo argumento cientos de veces en HN, y aun después de muchos comentarios recibidos durante ese tiempo, casi no se le ha agregado matiz.
No está completamente equivocado, pero tampoco completamente correcto. Muchas personas interesadas en este tema tuvieron muchas oportunidades, a lo largo de cientos de repeticiones, de mostrar ese punto, y aun así sorprende que la postura no haya evolucionado en absoluto. Esa actitud suena a una cerrazón patológica y hace perder el tiempo a todos los que participan en la conversación.
Creo que enfocarse en la solidez desvía la atención de técnicas que en la práctica han dado mejores resultados para el objetivo de tener software más correcto. Hay técnicas prácticas con respaldo teórico que a veces sorprenden incluso a quienes pensaban que la solidez era el único camino: http://users.csc.calpoly.edu/~gfisher/classes/509/handouts/h...
Esto se repite. Mientras los métodos sólidos logran mejoras importantes, los métodos no sólidos han conseguido en la práctica avances mucho mayores hacia software más correcto. Un ejemplo muy reciente es https://antithesis.com. Por supuesto, en ciertas situaciones las técnicas sólidas pueden ser más potentes y prácticas, así que es un tema complejo.
Es razonable esperar que se pueda verificar si las bibliotecas pequeñas de Rust usan correctamente unsafe. Eso por sí solo ya sería realmente útil.
También acabo de dejar un comentario relacionado en el artículo sobre F*. Viendo solo la sintaxis, subjetivamente prefiero F*/F# a Rust, pero decidí usar Ada/SPARK2014 para el software de control de shows que estoy desarrollando.
Para que Rust atraiga a la misma gente que Ada/SPARK2014, necesita un estándar oficial publicado, como los lenguajes existentes C, Common Lisp, Prolog, Fortran y COBOL. AdaCore y Ferrous Systems están colaborando para ofrecer herramientas de verificación formal para Rust como las de Ada/SPARK2014, así que Rust también está entrando en ese terreno, pero todavía no tiene un estándar publicado, y el legado de Ada y SPARK2014 es enorme.
Es interesante verlo como una especie de GC optimizado de ejecución inmediata que funciona cuando el conteo de referencias se usa estrictamente con datos acíclicos, o cuando se pueden aceptar fugas cíclicas. Python usa el enfoque híbrido de conteo de referencias + rastreo descrito en el artículo, y he visto despliegues en producción que obligan a ejecutar el recolector por rastreo solo una vez cada N solicitudes.
Perl usa conteo de referencias puro, pero tiene referencias débiles, así que al precio de preocuparse por qué parte de una estructura cíclica mantiene la referencia, se pueden volver los datos acíclicos desde la perspectiva del conteo de referencias. En teoría, Koka usa conteo de referencias, pero en la práctica intenta llevarlo lo más posible a tiempo de compilación; si en y = x + 1 se garantiza que x tiene una sola referencia y no se usará después, puede reutilizar el mismo almacenamiento para y y modificarlo in situ.
Nim ofrece ORC, que combina conteo automático de referencias con una implementación del algoritmo Recycler de Bacon+Rajan. Este algoritmo está diseñado para recolectar solo ciclos en sistemas basados en conteo de referencias, por lo que es bastante rápido. Volviendo a Rust, aquí hay una implementación stop-the-world de Recycler: https://github.com/fitzgen/bacon-rajan-cc y este fork la distribuye como el crate bacon-rajan-ccc: https://github.com/mbartlett21/bacon-rajan-cc La sección Alternative del README enlaza otros experimentos en la misma área. Si cuesta encontrar el paper de Recycler, reuní copias en https://trout.me.uk/gc/, y si tienen gustos parecidos, quizá también disfruten los papers en https://trout.me.uk/lisp/.
Firefox también usa conteo de referencias junto con un recolector de ciclos basado en trial deletion para gestionar ciclos entre objetos DOM en C++ y JS. De hecho, Graydon estuvo a cargo de la implementación inicial.
La verificación formal de programas me genera impaciencia. Demostrar que un programa implementa correctamente una especificación es interesante en teoría, pero tiene poca utilidad práctica.
Escribir una especificación correcta es tan difícil como programar correctamente, así que el problema difícil no se resuelve, solo se traslada. Hay usos prácticos de los métodos formales, pero son raros.
Eso es cierto si hablamos de una especificación completa, pero ese no suele ser el objetivo real. Normalmente lo que se quiere demostrar son algunas propiedades clave. Por ejemplo, que esta función siempre termina, o que aquella función siempre devuelve un arreglo ordenado.
Una vez que se puede hacer eso, se puede exigir como precondición. Por ejemplo, tener que demostrar que un arreglo ya está ordenado antes de pasarlo a una función.
Fue escrito el 15 de mayo de 2024, día del noveno aniversario de Rust 1.0.
Leí el artículo enlazado de Boats y me pareció excelente. Me sorprendió que la cita de Hoare de hace 50 años siga siendo relevante y esté tan bien expresada.
Me gustaría poder usar algo más simple, como type guards en tiempo de compilación. Cuando proliferan los trait bounds, los programas a nivel de tipos se vuelven difíciles de leer.
Por ejemplo, cosas como Where <<::Output as G>::Output as H>::Output: HList + Z o type Output = <<::Output as G>::Output as H>::Output;. Luego se le mete Cons>>>, y uno se da cuenta de que números como U8 de TypeNum también son, internamente, anidamientos de Cons>>. Se puede avanzar en esta área y conseguir las verificaciones deseadas, pero los mensajes de error pueden terminar siendo muy distintos de la forma en que un desarrollador humano escribe el código, y la implementación también es muy dolorosa.
La razón por la que la experiencia de desarrollo resulta sorprendente es que esto no es “solo una función”, sino una combinación concreta de genéricos y tipos asociados. Quería usar comprobaciones al estilo runtime, pero ejecutarlas en tiempo de compilación; para lograrlo, tuve que escribir código bastante distinto. Al final, hacer que el Rust en tiempo de compilación a nivel de tipos sea más simple, funcional y legible podría ser la forma de que estos proyectos de análisis formal ofrezcan una buena experiencia tanto a mantenedores como a usuarios. En resumen, quiero Rust con comptime. Y también me pregunto si Future basado en Pin<&mut Self> ya quedó consolidado. Me gustaría experimentar con otra implementación interna de async/await, pero no sé por dónde empezar.
1 comentarios
Opiniones de Hacker News
Buen artículo. Desde mi experiencia previa con verificación de programas, Rust parece el lenguaje moderno más útil para aplicar técnicas formales.
Las reglas de Rust eliminan muchos casos difíciles de formalizar. El gran problema que queda es el análisis de interbloqueos desde la perspectiva de los hilos y desde la perspectiva de
Rc/préstamos; ambas son, en cierta medida, equivalentes. Si Rust tuviera análisis estático de interbloqueos, creo que también serían posibles los punteros de desreferenciación seguros, y si se pudiera demostrar que todas las llamadas borrow/upgrade no fallan, se podría eliminar la mayoría del conteo de referencias. Entonces, en los casos posibles, la mutabilidad interna también saldría gratis.El gran problema de los demostradores de teoremas es que, como los construyen personas a las que les gusta demostrar teoremas, caen en el formalismo y su sentido de UI queda desalineado con el de los programadores. La mayoría de las obligaciones de prueba se pueden manejar con un solucionador SAT, pero los problemas difíciles requieren herramientas más pesadas. Coq es demasiado manual, y el autor considera que ACL2 es demasiado funcional. El aprendizaje automático puede ayudar a orientar a los demostradores de teoremas. Es difícil encargarle la prueba en sí, pero parece posible inferir planes de prueba en código donde el flujo de control y el uso de datos son, en general, parecidos.
Las rutinas criptográficas de Firefox y Wireguard no están escritas en Rust, sino en F*, más precisamente en Low*, un DSL de bajo nivel incorporado en F*, y están completamente verificadas.
https://project-everest.github.io/
https://mitls.org/
El problema al aplicar estas herramientas a la verificación de lenguajes externos como Rust es que las pruebas no se escriben en el lenguaje objetivo, por lo que el desarrollador tiene que aprender dos lenguajes. A partir de mi experiencia escribiendo Creusot, del trabajo en Verus y Aeneas, y de la experiencia en el laboratorio de Why3, he estado pensando en cómo se vería un “Rust consciente de la verificación”. Si se creara un lenguaje así desde el principio, su facilidad de verificación podría mejorar por etapas incluso respecto de Rust, y creo que sería especialmente efectivo en las partes difíciles de las pruebas.
Lo que más echo de menos como función integrada es algo equivalente a “ejecuta quickcheck sobre mi prueba”. Cuando tienes código e intentas demostrar una propiedad que no es verdadera, es fácil arrancarse los pelos sin entender por qué la prueba no sale. Si en medio de una prueba se llega a un estado sin sentido, sería bueno que un comando como “genera un contraejemplo aquí” devolviera un contraejemplo. Las pruebas dependen mucho del camino seguido y, en general, no son fáciles, pero estas herramientas parecen estar muy cerca de la grandeza. El proceso de intentar demostrar código también debería reflejar la posibilidad de que ese código tenga bugs.
El demostrador no deriva una prueba incorrecta; simplemente no logra derivar una prueba válida. Creo que no hay muchas aplicaciones de aprendizaje automático con esa propiedad.
En realidad, en Rust los locks y el conteo de referencias son estructuras en tiempo de ejecución.
Arcrompe bastante el modelo RAII de Rust, hasta el punto de que hubo que eliminar los scoped threads cuyos destructores debían ejecutarse antes de que terminara el scope. El conteo global de referencias tiene problemas de ciclos y fugas, y vuelve a ser un problema global. Probablemente sea difícil eliminarlo por completo, pero creo que es mejor encerrarlo en scopes estilo arena. Para los locks parecen necesarias estructuras de datos asimétricas, como los canales. En Go, los canales se dividen en emisor y receptor, y en la goroutine emisora se puede ponerdefer close(ch); incluso si hay un panic, se garantiza que se ejecutará cuando termine el resto del hilo. No tiene que ser necesariamente un canal, pero separar los roles de lectura-escritura/productor-consumidor hace que el razonamiento sea mucho más fácil y también parece ayudar al análisis formal.Me gusta que haya empezado con una cita del artículo de Hoare de alrededor de 1973 y que ahora ya haya llegado hasta un segundo texto. Originalmente dejé un comentario largo en el hilo de HN del artículo de boat, diciendo que inclinar esa cita hacia una perspectiva centrada en Rust es comprensible dado el trasfondo de boat, pero que reduce artificialmente el alcance de la crítica de Hoare
Ahora Grayson tomó ese fragmento estrecho como punto de partida para discutir algunas áreas interesantes y puntos de diseño de Rust. Sigo pensando que mi comentario era correcto, pero la discusión que surgió del texto de Grayson fue suficiente para compensar mis objeciones técnicas al texto que sirvió de punto de partida
Desde entonces, con la aparición de técnicas no sólidas más avanzadas que las pruebas simples, creo que los métodos no sólidos terminaron adelantándose a los métodos sólidos
Identificó el problema y, visto en retrospectiva, la solución de imponer compartición XOR mutabilidad mediante el sistema de tipos parece un pequeño paso. Si en ese momento se hubiera descubierto que ese pequeño paso era la solución, se habría evitado una enorme cantidad de sufrimiento durante 50 años
Pero no me parece que la cita en sí refuerce esa perspectiva. Se puede ver como un intento de tomar el lamento más general de Hoare sobre la existencia semántica misma de las referencias y aplicarlo al modelo de estado mutable sin alias de Rust para esquivar el problema. Sin embargo, eso se parece más a arreglar un fragmento estrecho de un problema mayor y decir que todo el problema desapareció. Las partes omitidas, en especial el comienzo de la sección “Variables” y el ejemplo de ALGOL 68, se inclinan mucho más hacia la idea de que Hoare criticaba no solo el estado mutable, sino el propio concepto semántico de referencia. Reconozco el intento de Rust de domesticar una parte del problema, pero no creo que ningún lenguaje lo haya “arreglado”
No entiendo muy bien por qué este texto recibe tantos elogios. Siento que despacha varias áreas del análisis de programas en un solo párrafo. Me gusta Graydon y respeto su perspectiva, pero este párrafo está demasiado simplificado
La explicación de que los lenguajes con GC no se molestaron en ofrecer un soporte fuerte para el razonamiento local es un hombre de paja. Hubo lenguajes como Pony, que usan GC y aun así incorporan regiones en el sistema de tipos. Además, existen campos completos como el análisis de punteros y el análisis de escape, que infieren unicidad y determinan si dos referencias pueden ser alias. El núcleo del tipado estático también consiste en dividir el heap en partes que no se aliasan entre sí mediante la técnica de clases y campos. No estamos hablando de JavaScript, y no deberíamos fingir que Java/C#/Scala y muchísimos lenguajes con GC carecen de razonamiento local sobre el estado mutable
Las clases y los campos no ofrecen razonamiento local completo sobre el estado mutable, porque una clase/objeto A puede llegar a depender del estado mutable de una clase/objeto B. La herencia de clases al estilo Java añade por sí sola aún más complejidad a medida que el programa evoluciona con el tiempo
Claro que hay contraejemplos, pero si miramos lenguajes de propósito general con GC y de uso masivo como Java, C# y Python, la afirmación es correcta. Es posible interpretar que la idea original de la orientación a objetos se parecía más al modelo de actores actual, y que pretendía modificar estructuras de datos con dueño únicamente mediante paso de mensajes. Pero las implementaciones reales de la orientación a objetos casi no se acercan a ese objetivo. Java no impide guardar referencias mutables al mismo objeto en varios objetos. Este artículo lo explica mejor: https://without.boats/blog/references-are-like-jumps/
void myMethod(final Map map) { map.remove("key"); int oldSize = map.size(); map.put("key", "val"); int newSize = map.size(); System.out.println(newSize - oldSize); }Edición: leí mal la doble negación. Incluso al releerlo, todavía me resulta confuso. ¿Quiere decir que Java, a diferencia de JavaScript, sí tiene razonamiento local?
Por lo general me gustan los textos de Graydon, pero este, como muchos artículos sobre técnicas formales, puede dar una impresión equivocada a lectores que no conocen el campo. Es parecido a decir que el método para convertir plomo en oro mejoró en una escala de un dígito, sin decir que todavía faltan 29 órdenes de magnitud para que sea práctico y costo-efectivo.
¿Que no tener aliasing facilita mucho la verificación formal? Sí. ¿Que por eso se puedan verificar programas reales de forma práctica y costo-efectiva? Para nada. Hay programas, circuitos y componentes que se verifican formalmente todos los días, pero son más bien excepciones, relativamente muy pequeños y construidos de una manera especialmente cuidadosa. Las propiedades que ayudan al razonamiento local son importantes, pero no cambian de forma sustancial cómo garantizar de manera sólida la corrección del software mainstream.
Incluso los programas en un lenguaje lejos de ser Turing completo —sin heap, sin punteros, sin enteros, solo variables booleanas y con bucles que no pueden ejecutarse más de dos veces— no se pueden verificar en la práctica porque se reducen a TQBF. Para ciertas propiedades, por ejemplo la seguridad de memoria, sí puede ser posible, pero no alcanza para lo que necesita el software. En los años 70 a 90 existía la esperanza de que, aunque la complejidad del peor caso fuera intratable, las garantías locales y la estructura del lenguaje nos alejarían del peor caso; después se demostró que no era así. La esperanza de que los programas que la gente realmente escribe estén lo suficientemente lejos del peor caso como para que surjan buenas heurísticas tampoco parece sostenerse ya.
Hay una charla relacionada sobre esto: https://pron.github.io/posts/correctness-and-complexity
El resultado clave es que la mayoría de las propiedades interesantes que uno querría verificar no son composicionales. Aunque se demuestre una propiedad para cada componente P1...Pn, el costo de demostrar esa propiedad para P1 ○ ... ○ Pn no solo crece de forma superpolinómica respecto de n, sino también respecto del tamaño de cada componente. Es decir, es tan difícil como si no se hubiera dividido, y la corrección no se descompone. Por eso “se pueden verificar bastantes cosas” y “lo verificable es una gota en el océano” pueden ser ambas afirmaciones verdaderas, y en las discusiones sobre técnicas formales a menudo se omite esa brecha.
No está completamente equivocado, pero tampoco completamente correcto. Muchas personas interesadas en este tema tuvieron muchas oportunidades, a lo largo de cientos de repeticiones, de mostrar ese punto, y aun así sorprende que la postura no haya evolucionado en absoluto. Esa actitud suena a una cerrazón patológica y hace perder el tiempo a todos los que participan en la conversación.
Esto se repite. Mientras los métodos sólidos logran mejoras importantes, los métodos no sólidos han conseguido en la práctica avances mucho mayores hacia software más correcto. Un ejemplo muy reciente es https://antithesis.com. Por supuesto, en ciertas situaciones las técnicas sólidas pueden ser más potentes y prácticas, así que es un tema complejo.
unsafe. Eso por sí solo ya sería realmente útil.También acabo de dejar un comentario relacionado en el artículo sobre F*. Viendo solo la sintaxis, subjetivamente prefiero F*/F# a Rust, pero decidí usar Ada/SPARK2014 para el software de control de shows que estoy desarrollando.
Para que Rust atraiga a la misma gente que Ada/SPARK2014, necesita un estándar oficial publicado, como los lenguajes existentes C, Common Lisp, Prolog, Fortran y COBOL. AdaCore y Ferrous Systems están colaborando para ofrecer herramientas de verificación formal para Rust como las de Ada/SPARK2014, así que Rust también está entrando en ese terreno, pero todavía no tiene un estándar publicado, y el legado de Ada y SPARK2014 es enorme.
Es interesante verlo como una especie de GC optimizado de ejecución inmediata que funciona cuando el conteo de referencias se usa estrictamente con datos acíclicos, o cuando se pueden aceptar fugas cíclicas. Python usa el enfoque híbrido de conteo de referencias + rastreo descrito en el artículo, y he visto despliegues en producción que obligan a ejecutar el recolector por rastreo solo una vez cada N solicitudes.
Perl usa conteo de referencias puro, pero tiene referencias débiles, así que al precio de preocuparse por qué parte de una estructura cíclica mantiene la referencia, se pueden volver los datos acíclicos desde la perspectiva del conteo de referencias. En teoría, Koka usa conteo de referencias, pero en la práctica intenta llevarlo lo más posible a tiempo de compilación; si en
y = x + 1se garantiza quextiene una sola referencia y no se usará después, puede reutilizar el mismo almacenamiento parayy modificarlo in situ.Nim ofrece ORC, que combina conteo automático de referencias con una implementación del algoritmo Recycler de Bacon+Rajan. Este algoritmo está diseñado para recolectar solo ciclos en sistemas basados en conteo de referencias, por lo que es bastante rápido. Volviendo a Rust, aquí hay una implementación stop-the-world de Recycler: https://github.com/fitzgen/bacon-rajan-cc y este fork la distribuye como el crate bacon-rajan-ccc: https://github.com/mbartlett21/bacon-rajan-cc La sección Alternative del README enlaza otros experimentos en la misma área. Si cuesta encontrar el paper de Recycler, reuní copias en https://trout.me.uk/gc/, y si tienen gustos parecidos, quizá también disfruten los papers en https://trout.me.uk/lisp/.
La verificación formal de programas me genera impaciencia. Demostrar que un programa implementa correctamente una especificación es interesante en teoría, pero tiene poca utilidad práctica.
Escribir una especificación correcta es tan difícil como programar correctamente, así que el problema difícil no se resuelve, solo se traslada. Hay usos prácticos de los métodos formales, pero son raros.
Una vez que se puede hacer eso, se puede exigir como precondición. Por ejemplo, tener que demostrar que un arreglo ya está ordenado antes de pasarlo a una función.
Fue escrito el 15 de mayo de 2024, día del noveno aniversario de Rust 1.0.
Leí el artículo enlazado de Boats y me pareció excelente. Me sorprendió que la cita de Hoare de hace 50 años siga siendo relevante y esté tan bien expresada.
Me gustaría poder usar algo más simple, como type guards en tiempo de compilación. Cuando proliferan los trait bounds, los programas a nivel de tipos se vuelven difíciles de leer.
Por ejemplo, cosas como
Where <<::Output as G>::Output as H>::Output: HList + Zotype Output = <<::Output as G>::Output as H>::Output;. Luego se le meteCons>>>, y uno se da cuenta de que números comoU8de TypeNum también son, internamente, anidamientos deCons>>. Se puede avanzar en esta área y conseguir las verificaciones deseadas, pero los mensajes de error pueden terminar siendo muy distintos de la forma en que un desarrollador humano escribe el código, y la implementación también es muy dolorosa.La razón por la que la experiencia de desarrollo resulta sorprendente es que esto no es “solo una función”, sino una combinación concreta de genéricos y tipos asociados. Quería usar comprobaciones al estilo runtime, pero ejecutarlas en tiempo de compilación; para lograrlo, tuve que escribir código bastante distinto. Al final, hacer que el Rust en tiempo de compilación a nivel de tipos sea más simple, funcional y legible podría ser la forma de que estos proyectos de análisis formal ofrezcan una buena experiencia tanto a mantenedores como a usuarios. En resumen, quiero Rust con
comptime. Y también me pregunto siFuturebasado enPin<&mut Self>ya quedó consolidado. Me gustaría experimentar con otra implementación interna deasync/await, pero no sé por dónde empezar.