Lean 4.22: Una Nueva Infraestructura de Verificación para Programas Imperativos
Lean 4.22 presenta una característica nueva y emocionante: una nueva infraestructura de verificación para probar propiedades de programas imperativos. La publicación utiliza un ejemplo simple, determinar si una lista contiene dos enteros que suman cero, para demostrar el uso de la característica y la compara con herramientas similares como Dafny y Verus. El nuevo marco, Std.Do, utiliza triples de Hoare y combina las tácticas `mvcgen` y `grind` para simplificar enormemente el proceso de verificación para programas imperativos, incluso aquellos con un flujo de control complejo como bucles y devoluciones anticipadas. A diferencia de los sistemas automatizados que dependen de solucionadores SMT externos, el enfoque de prueba interactiva de Lean ofrece mayor confiabilidad, depuración más fácil y mejor mantenimiento, lo que lo convierte en una opción convincente para las tareas de verificación de programas del mundo real.