haskell - Los tipos dependientes pueden demostrar que su código es correcto hasta una especificación. Pero, ¿cómo demuestras que la especificación es correcta?

agda dependent-type (7)

¿Cómo se prueba que las matemáticas son correctas? Es decir, ¿cómo se demuestra que la suma entera es la forma correcta de contar manzanas, o cómo se prueba que la adición real es la forma correcta de agregar pesos? Siempre hay una interfaz entre lo formal / matemático y lo informal / real. Requiere habilidad y gusto matemático / físico para encontrar el formalismo apropiado para resolver un problema en particular. Los métodos formales no eliminarán eso.

El valor de los métodos formales es doble:

No sabrá si su programa es correcto, a menos que sepa qué propiedades realmente satisface. Antes de saber si su rutina de clasificación es "correcta", primero debe saber lo que realmente hace. Cualquier procedimiento para descubrirlo será un método formal (¡incluso pruebas unitarias!), Por lo que las personas que rechacen los "métodos formales" simplemente se limitan a un pequeño subconjunto de los métodos disponibles.
Incluso cuando sabes cómo saber qué es lo que un programa realmente hace, la gente comete errores en su razonamiento matemático (no somos criaturas racionales, independientemente de lo que afirmen ciertas ideologías); así que es útil que una máquina nos controle. Esta es la misma razón por la que utilizamos pruebas unitarias: es agradable ejecutar una verificación de escritorio y asegurarnos de que el programa haga lo que queremos; pero hacer que la computadora controle y decirnos si el resultado es correcto ayuda a prevenir errores. Dejar que la computadora verifique nuestras pruebas sobre el comportamiento del programa es útil por exactamente la misma razón.

Los tipos dependientes a menudo se anuncian como una forma de permitirle afirmar que un programa es correcto hasta una especificación. Entonces, por ejemplo, se le pide que escriba un código que ordene una lista : puede probar que el código es correcto codificando la noción de "ordenar" como un tipo, y escribiendo una función como List a -> SortedList a . Pero, ¿cómo se demuestra que la especificación, SortedList , es correcta? ¿No sería el caso que, cuanto más compleja sea su especificación, más probable será que su codificación de esa especificación como un tipo sea incorrecta?

Creo que es al revés: un programa bien tipado no puede probar tonterías (suponiendo que el sistema sea consistente), mientras que las especificaciones pueden ser inconsistentes o simplemente tontas. Entonces, ¿no es "cómo asegurarse de que este fragmento de código refleje mis ideas platónicas", sino "cómo asegurarme de que mis ideas se proyecten de manera significativa en un plano bien fundado de reglas sintácticas puras"? ¿Cómo asegurarse de que el pájaro que ves es un sinsonte [por alguna noción de merodeado suministrado]? Bueno, estudia las aves y aumenta las posibilidades de que tengas razón. Pero como always con los humans , no can''t estar 100% seguro.

La teoría de tipos es una forma de mitigar la imperfección de la mente humana mediante la introducción de reglas formales, pruebas verificadas por máquina (es un documento muy relevante) y otras cosas, que permiten enfocarse y simplificar mucho los problemas (como dijo Brouwer: "Matemáticas es nada más y nada menos que la parte exacta de nuestro pensamiento "), pero no se puede esperar que ninguna herramienta haga" correctos "tus pensamientos, porque simplemente no existe una noción uniforme de lo correcto. IOW, no hay forma de conectar formalmente informal y formal: ser informal es como estar dentro de la mónada IO : no hay escapatoria.

Entonces, no es "¿esta sintaxis refleja mi semántica muy precisa?", Sino más bien "¿puedo adjuntar mi semántica en bruto a esta sintaxis fuertemente estructurada?". Los programas son objetos materiales adecuados, mientras que las ideas son aproximaciones engorrosas, que pueden convertirse en objetos materiales adecuados solo por convención. Así que formamos una base usando convenciones, y luego solo confiamos en ello, porque es mucho más sensato confiar en un pequeño subconjunto de todas sus numerosas ideas que en todas ellas.

Esta es la versión estática del sistema de tipos de: ¿Cómo dice que sus pruebas son correctas?

La única respuesta que puedo dar honestamente es, sí, cuanto más compleja y poco manejable sea su especificación, más probable es que haya cometido un error. Puedes equivocarte al escribir algo en un formalismo teórico de tipos tan bien como puedas al formalizar la descripción de tu programa como una función ejecutable.

La esperanza es que su especificación sea lo suficientemente simple como para juzgar mediante un examen, mientras que su implementación podría ser mucho más amplia. Es útil que, una vez que haya formalizado algunas ideas "semilla", pueda demostrar que las ideas derivadas de ellas son correctas. Desde ese punto de vista, cuanto más fácilmente pueda derivar mecánica y probadamente partes de su especificación de partes más simples, y en última instancia derivar su implementación de su especificación, es más probable que obtenga una implementación correcta.

Pero puede no estar claro cómo formalizar algo, lo que tiene el efecto de que o bien puede cometer un error al traducir sus ideas al formalismo - puede pensar que probó una cosa, cuando en realidad probó otra - o puede que se encuentre haciendo un tipo investigación teórica para formalizar una idea.

Este es un problema con cualquier lenguaje de especificación (incluso inglés), no solo con tipos dependientes. Su propia publicación es un buen ejemplo: contiene una especificación informal de "función de clasificación" que solo requiere que se ordene el resultado, que no es lo que desea ( /xs -> [] calificaría). Ver, por ejemplo, esta publicación del blog de Twan van Laarhoven.

Llegando tarde a la fiesta, pero AFAICT, nadie ha mencionado otro aspecto importante: en el contexto de la verificación del programa, tener un error en la especificación no siempre es demasiado terrible, porque puede usar el código para verificar la especificación .

IOW, la prueba no dice "el código es correcto", pero "el código y la especificación son mutuamente consistentes". Entonces, para que un error en la especificación pase desapercibido, tiene que ser uno de:

una especificación no especificada
un error en la especificación que coincide con un error correspondiente en el código.

Como alguien más señaló: el problema es el mismo para las pruebas.

Supongamos que su función no es de nivel superior uno, sino que la usa alguien más como parte de algún módulo, que también tiene una prueba de corrección. Este último debe usar pruebas de corrección de su función, y si es malo, el módulo no compilará. El módulo en sí todavía puede tener errores, pero ya no es problema suyo.

Una cosa que pueden hacer los métodos formales que no creo que otros hayan tocado es ayudar a relacionar cosas simples con otras más complejas. Puede que no sepa con certeza cómo especificar exactamente cómo se comportaría una estructura de datos de Set , pero si puede escribir una versión simple basada en listas ordenadas, puede probar que su versión elegante basada en árboles de búsqueda equilibrada se relaciona correctamente con el Función toList Es decir, puede usar métodos formales para transferir su confianza en listas ordenadas a árboles de búsqueda equilibrada.