Como os lo cuento. Llevaba una semanita o por ahí dándole vueltas a que ya iba siendo hora de abrir la temporada de pantalon corto. Hoy he hecho betatesting del tiempo y ya a medio día he alcanzado la conclusíon de que es buen momento para hacerlo oficialmente. Sigue haciendo un frío del carajo, y no hay valor para quitarme ni la camiseta de manga corta, ni la de manga larga, ni la sudadera, pero ir enseñando las canillas no es mal plan. Además que he cambiado de zapatillas, y estas me aisla bien del suelo, por lo que a fin de cuentas hasta se agradece un poco de, como diría Rita, fresquet en las calves, plural de calf, que además de res, es como llaman a los gemelos en el habla local.
En otro orden de cosas ando aprendiendo a hacer programación certificada a traves de tipos dependientes (CPDT). Javi, te recomiendo esa mierda. El certificado no se refiere a una titulación que alguna entidad expide, como Cisco u Oracle (java) o a el cumplimiento de un estandar. Se refiere a programas verificados formalmente. Hacer un programa y probarlo para un puñado de posibles entradas y que no se ropa es (en cierta medida) fácil. Incluso automatizar la batería de pruebas para que cuando la gente toca por aquí y por allá ver que no se ha roto nada. Pero ya dijo Dijkstra, entre tantas otras cosas, que las baterías de pruebas sólo sirven para demostrar incorrección y no corrección. Así que el siguiente paso es la verificación formal, es decir, la prueba matemática, lo cual requiere expresar tu programa en términos matemáticos. Y en las matemáticas el concepto de estado tan común en la computación es inexistente ya que el objeto que más frecuentemente se usa es la función, entendida como una correspondencia entre los elementos de un conjunto de origen o de saliday los de un conjunto de llegada. Así como ejemplo sencillito pensamos en la suma: Todos conocemos la funcion "suma 1", que a cada número le asocia el siguiente. Del mismo modo tenemos la función "suma 33" que pone en correspondencia al 1 con el 34, al 7 con el 40 y ya sabéis como sigue esto. Ahora, en esta formalización, si queremos pensar en la suma binaria de toda la vida (la que coge dos números y los suma), la tratamos como una funcíon con conjuto de salida los naturales (por hacerlo sencillo) y como conjunto de llegada "las funciones con conjunto de salida los naturales y conjunto de llegada los naturales". Espero que aún sigáis conmigo los que no os habíais encontrado nunca con estos términos. En ese caso, la funcion de suma binaria hace corresponder a cada natural n la función "suma n", de manera que evaluar la expresión:
suma_binaria 33 7
Que avezados matemáticos nostros ya sabemos que da 40, pero lo bonito no es el resultado en sí, si no su construcción. El primer paso es aplicar la función suma_binaria a 33, que tiene como resultado la funcion "suma 33", que a su vez se aplica sobre el 7, y como ya hemos dicho en el preámbulo, lo manda al 40. Esta forma de considerar las funciones como transformaciones que toman un objeto y devuelven otro objeto, donde los objetos viven en un mundo bastante rico que contiene entre otros, pero no se limita a, números, conjuntos de números y funciones, se llama currificación no por las especias si no por Curry, una de las personas más prolíficas en el área. Esta concepción de la que os hablo simplifica mucho ciertas cosas.
Y el caso es que podemos hacer artificios que propaguen estado en forma de argumentos de funciones, podemos emular la toma de decisiones con funciones definidas a trozos, y la concepción de los naturales de Peano viene en nuestra ayuda para cuando queremos repetir algo unas cuantas veces.
Y una vez nuestro programa está expresado en estos términos, tenemos herramientas que nos ayudan a hacer la demostracíon de que nuestro programa es correcto, o nos muestras que proposiciones (o propiedades) del programa hacen que no lo sea, de manera que podemos solucionarlas, incluso aunque no seamos capaces de crear un caso de prueba que exponga ese comportamiento indeseado.
Vamos una fumada, pero uno de los compis de curro dijo que iba a leerse un libro para aprender, y que si alguien se apuntaba, y oye, pues por qué no.
Espero que no hayáis hecho un TLDR :) Buen finde!
No hay comentarios:
Publicar un comentario