C*: un lenguaje que unifica programación y verificación formal en C
C*: Unifying Programming and Verification in C
C* es un diseño de lenguaje que integra la verificación formal directamente en la programación en C. Extiende C con capacidades de verificación basadas en un motor de ejecución simbólica y un núcleo de prueba estilo LCF, permitiendo a los programadores insertar bloques de código de prueba junto al código de implementación y actualizar el estado de la prueba de forma interactiva. Su soporte de pruebas expresivo y extensible permite construir bibliotecas reutilizables de definiciones lógicas, teoremas y automatización de pruebas programable. Al usar C como lenguaje común, C* unifica el desarrollo de código de implementación y de prueba, haciendo que la verificación sea accesible para programadores convencionales. El prototipo fue evaluado con un conjunto de programas pequeños y un caso de estudio real: la función attach del asignador de compañeros de pKVM, demostrando su capacidad para manejar una amplia gama de modismos de programación en C y tareas de razonamiento complejas.
Un obstáculo clave para la participación de los programadores en las prácticas de verificación es la desconexión de entornos y paradigmas entre las prácticas de programación y verificación, lo que limita la accesibilidad y la verificación en tiempo real.
- eggy
He estado en este tema desde hace tiempo. Me he decidido por aprender Ada/SPARK. Ada 2022 comenzará a alimentar una nueva actualización de SPARK 2014. Sí, ambos son verbosos, si no te gusta ese tipo de cosas, y no te gusta la sintaxis tipo Pascal. Créeme, me gustan APL/J/k/uiua/BQN y Forth y ASM. Normalmente soy agnóstico en cuanto a sintaxis siempre que el lenguaje y el ecosistema (más importante de lo que muchos piensan) satisfagan tus necesidades. Probé Rust en 2018, y luego de nuevo en 2023, pero lo encontré muy complejo y, bueno, no soy fan de su sintaxis. Habría preferido una sintaxis más estilo ML o Haskell. Zig parecía agradable, pero es un caso de uso diferente y demasiado nuevo. Después de todo, Ada/SPARK han estado en aplicaciones enormes, de alta confiabilidad y alta seguridad durante décadas. Rust está recibiendo parte de ese amor, y viceversa. AdaCore había creado un compilador de Rust verificado, pero con un producto del mundo real (polipasto Blacktail) en desarrollo, necesitamos un conjunto de herramientas y garantías y facilidad de auditoría y aceptación para lograr altas certificaciones de seguridad y estándares. Piensa en aeroespacial, defensa, ferrocarril y automoción. Empecé a programar en 1977, así que siempre hay un lugar en mi corazón para ASM/C. Jugué con F#, F* y LOW de Microsoft, y son buenos, pero ellos y Rust simplemente no tienen el legado del mundo real de Ada/SPARK. He estado usando Shen para escribir algunos modelos verificados formalmente de áreas menos críticas para la seguridad de nuestro software y lo encuentro refrescante, sin embargo, mi trabajo diario es mantenerme enfocado en Ada/SPARK hasta que Rust madure más con un compilador verificado formalmente y probado.
- IsTom
Me gusta el concepto de lógica de separación tanto como al siguiente, pero no creo que esto lo sea. Solo mira los ejemplos, con invariantes de bucle que por sí solos son más largos que todo el ejemplo. No es solo un problema de ergonomía, sino que deja mucho espacio para errores de especificación.
Y sospecho que la intersección de personas que escriben código C que quieres verificar con gente de verificación formal no es particularmente grande.
- gavinray
Realmente creo que los lenguajes conscientes de la verificación se van a convertir en una necesidad.
Escribí un poco sobre esto recientemente.
https://gavinray97.github.io/blog/design-by-contract-and-eff...
- slowcache
Creo que la verificación formal es un campo súper interesante, pero esto no es viable para mí porque no tengo una E al revés en mi teclado.
- Taikonerd
Los autores citan esto, pero solo para mencionarlo: esto suena como F*, otro lenguaje orientado a pruebas. (https://fstar-lang.org/)
F* es de la familia ML de lenguajes, por lo que se ve bastante diferente de C*.