Esa es una pregunta bastante difícil de responder. Depende íntimamente de lo que quieras probar.
Sin embargo, se simplifica por la pureza de un lenguaje (como lo es Haskell) en el sentido de que puedes razonar por igualdad. Entonces, si tiene e1 y e2 y puede demostrar que e1 es igual a e1 ′ y e2 es igual a e2 ′, entonces también e1 e2 es igual a e1 ′ e2 ′, la idea de que puede reemplazar iguales por iguales. Dado que los cálculos no tienen efectos secundarios en un lenguaje puro, obtiene dicha garantía.
En mi curso de programación funcional, enseño a los estudiantes cómo probar las propiedades de las funciones que funcionan en listas, como map (f. G) xs = map f (map g xs), lo que significa que puede fusionar mapas en un solo mapa, y Dada nuestra intuición de lo que hace el mapa, esto es algo que espera mantener. De esta forma, puede probar un conjunto de propiedades para una función, y puede probar que su función tiene todas las propiedades que necesita para ser la función que deseaba (por ejemplo, para una implementación de clasificación particular que podría probar que la lista de entrada y salida contiene los mismos valores (exactamente el mismo número de veces), y que la lista de salida aumenta de acuerdo con el operador de comparación que utiliza, lo que implica que su función es una función de clasificación). Y varios otros tipos de propiedades. Estos son típicamente probados por inducción. Además, puede usar técnicas similares habituales, o simplemente razonamiento igual para probar las leyes de mónada y otras propiedades relativamente simples. Las estructuras más complicadas exigirán formas más complicadas de razonamiento.
- ¿Cuál es el beneficio de estudiar lógica y teoría de conjuntos para matemática o informática?
- ¿Cómo es útil la matemática (integral, pecado, cos) en la programación?
- ¿Cuáles son algunas aplicaciones del mundo real de min-cut en la teoría de grafos?
- Cómo formular matemáticamente para seleccionar los mejores valores de N de una matriz
- ¿Cómo funciona la distribución de probabilidad al construir una nueva variable aleatoria?
En cuanto a probar que los programas completos son “correctos”, me pregunto si alguien realmente hace eso. Tal vez, entonces, debería pasar a idiomas como Coq y Agda, idiomas dependientes.
Jur
