Creía que Allow sería un probador de teoremas, pero según leo en la F.A.Q. no lo es, de todas formas estuve leyendo un poco y ya me chocan unas cuantas cosas, como que hable de estados e invariantes "If it's a state invariant INV, for example, models of INV will be states that satisfy the invariant" y a la vez diga que Allow es un modelo declarativo, cuando un paradigma declarativo precisamente no posee el concepto de estado... ni conoce el significado de bucle o clase (yo al menos sólo he oido hablar de invariantes de bucle o de clase, y no se me ocurre otro contexto la verdad), o por ejemplo " Unlike a programming language, an Alloy model is declarative" ¿uhm? ¿Acaso no hay lenguajes de programación declarativos? Coño, ¿no conocen Prolog, Ocaml, ML, Haskell, ¡SQL!...? Sí ya sé que prolog es lógico y los otros tres funcionales y SQL relacional, pero los paradigmas lógico, funcional y relacional son declarativos.

Si alguien sabe de que habla y me dice en donde me equivoco se lo agradecería, me suena raro leer tanta contradicción (desde mis conocimientos).

De todas todas el artículo me parece interesante y yo aunque todavía estoy falto de experiencia soy totalmente partidario de la verificación formal de código, ya en su día, cuando en una noticia de este sitio se preguntaba por si era posible hacer SO's seguros, hice referencia a esto mismo. Y es que es normal, puedes aplicar metodologías, hacer mil pruebas... al final todo eso te da una seguridad que en la mayoría de los casos es aceptable, pero no lo es, según mi criterio, cuando hay cientos de vidas que dependen del software que estás creando. Al igual que al arquitecto no le queda más remedio que realizar un cálculo de estructuras el informático debería verificar la correción de su código. Lo primero que te dicen cuando te enseñan a probar programas (sí, incluso hay gente especializada en ello) es que 1) la prueba total es imposible 2) por lo anterior, las pruebas que dan resultados correctos no demuestran que no hay fallos, sino que no los has encontrado, de hecho se suele hablar de prueba satisfactoria cuando encuentras un error. La verificación formal SI te asegura que un programa es correcto para los infinitos casos posibles.

 ¿Cual es el problema? Pues seguramente una gran culpa lo tenga el hecho de que la mayoría de los programas se escriben en lenguajes operacionales (C, C++, Java, etc...), verificar formalmente un código asi es un infierno porque existen efectos colaterales, ¿solución?, lenguajes funcionales, cómodos, ágiles, poseen transparencia referencial... en fin, cojonudos, yo me enamoré de OCaml ;D

el saber nos hace libres

...dije Allow quise decir Alloy :$ Ni con previsualización me dí cuenta.

el saber nos hace libres