Traducción al español 
Documento Original publicado por Lars Brünjes, Director de Educación, el 26 de Septiembre de 2018
En IOHK, estamos orgullosos de nuestro enfoque científico y de nuestra estrecha colaboración con el mundo académico. Publicamos en revistas científicas revisadas por pares y presentamos nuestros resultados en conferencias internacionales aclamadas para asegurarnos de que nuestros protocolos y algoritmos se construyen sobre bases sólidas como una roca. Nuestro software debe reflejar esta excelencia y calidad científica, lo que significa que necesitamos un proceso para pasar de los resultados científicos al código real escrito en el lenguaje de programación Haskell. Por lo tanto, decidimos realizar una formación interna sobre “corrección funcional”, para que la calidad de nuestros fundamentos teóricos se traduzca en una calidad igual para nuestro código.
Hicimos el primer curso durante cuatro días en Regensburg, Alemania, hace dos semanas. Este entrenamiento está dirigido a todos los que escriben Haskell en IOHK, así que decidimos realizar cuatro sesiones, más o menos basadas en la geografía - hay ingenieros de IOHK en 16 países. Planeamos hacer una segunda sesión en Regensburg en noviembre y dos más a principios del próximo año en los Estados Unidos. Los conferenciantes fueron Andrés Löh, cofundador de la consultoría Well-Typed, y John Hughes, fundador de QuviQ, ambos destacados en el mundo Haskell.
John es uno de los creadores de Haskell y co-inventor de QuickCheck, la herramienta de pruebas de Haskell. La mayoría de las compañías de software (si es que hacen pruebas, lo cual, lamentablemente, no siempre es el caso), usan pruebas unitarias. Para ello, los desarrolladores escriben a mano una serie de pruebas, casos que consideran típicos o relevantes o interesantes, y luego utilizan un marco de pruebas unitarias para realizar las pruebas e informar si producen los resultados esperados. QuickCheck es diferente. En lugar de especificar un puñado de pruebas, los desarrolladores que utilizan QuickCheck indican las propiedades que debería tener su código. QuickCheck genera muchos casos de prueba aleatorios y comprueba la propiedad de cada uno de ellos. Si QuickCheck encuentra que una propiedad ha sido violada, primero intenta simplificar la prueba, y luego informa al usuario sobre el caso de fallo más simple.
Como ejemplo simple, digamos que usted escribió un programa para ordenar una lista de nombres. Usando pruebas unitarias, se puede comparar el programa con algunos ejemplos hechos a mano de listas de nombres (algo así como [“Tom”, “Dick”, “Harry”] y [“Dora”, “Caesar”, “Berta”, “Anton”]). Con QuickCheck, por otro lado, usted se sentaría y pensaría cuidadosamente acerca de las propiedades que su programa debería tener En el ejemplo de ordenar listas de nombres, ¿qué propiedades esperaría? Bueno, después de ejecutar el programa, debería obtener una lista ordenada alfabéticamente. Oh, y esa lista debería contener todos los nombres que introdujo. Y sí, sólo debe contener los nombres que introdujo. Puede escribir estas propiedades como programas de Haskell y luego entregarlas a QuickCheck. La herramienta comprueba sus propiedades contra tantas listas de nombres generadas al azar como desee (normalmente cientos o miles) e identifica cualquier violación.
Estudiantes de Haskell en clase
En la práctica, QuickCheck a menudo se las arregla para encontrar problemas que se pasan por alto con métodos menos rigurosos, porque sus autores tienden a pasar por alto casos oscuros y escenarios complicados. En nuestro ejemplo, pueden, por ejemplo, olvidarse de probar una lista vacía de nombres. O puede haber un error en el programa que sólo ocurre para listas largas de nombres, y sus pruebas unitarias sólo verifican las listas cortas. John tenía muchas `historias de guerra’ de esto sucediendo en la vida real con clientes reales, donde los errores sólo se revelaban después de una serie de complejas operaciones entrelazadas que ningún escritor de pruebas unitarias humano se hubiera imaginado.
Todos los desarrolladores de Haskell han oído hablar de QuickCheck y comprenden las ideas básicas, pero en programas complejos del mundo real como Cardano, a veces no es tan fácil usar la herramienta correctamente. Por lo tanto, fue estupendo que el propio John, que ha estado utilizando QuickCheck durante 20 años y ha trabajado con muchas industrias, incluyendo servicios web (Riak, Dropbox y LevelDB), servidores de chat (Ejabberd), compras en línea (Dets), automoción (Autosar specification) y telecomunicaciones (MediaProxy, Ericsson y Motorola), explicara las complejidades y los puntos más delicados. Ayuda a encontrar errores y garantiza la corrección todos los días. Dada la experiencia de John, los participantes en la formación pudieron pasar la mitad de su tiempo aprendiendo los puntos más finos de QuickCheck del propio maestro. Fue tremendamente divertido disfrutar del obvio entusiasmo de John y su profundo conocimiento del tema. El resto de la sesión se dedicó a comprender la relación entre las especificaciones formales, escritas en un estilo matemático, y las implementaciones de Haskell.
En IOHK, trabajamos muy duro para escribir el código correcto. Por ejemplo, especificamos el comportamiento y las propiedades del programa usando matemáticas rigurosas. Al final, por supuesto, no podemos desplegar las matemáticas en un ordenador. En cambio, nuestros desarrolladores tienen que tomar la especificación, traducir las matemáticas a Haskell y producir código ejecutable y eficiente. Este proceso es más fácil para Haskell, porque está firmemente arraigado en los principios matemáticos, que para la mayoría de los idiomas, pero sigue siendo un salto conceptual. La especificación habla de objetos matemáticos como conjuntos y relaciones, que deben traducirse en tipos de datos y funciones lo más fielmente posible. Nadie gana si tus hermosas matemáticas se “pierden en la traducción” y terminas con código con errores. Por ejemplo, cuando los matemáticos hablan de números enteros (…, -2, -1, 0, 1, 2,…) o números reales (como π, y √2), ¿cómo se expresa esto en Haskell? Hay tipos de datos como Int o Double que parecen relacionados, pero no son los mismos que los conceptos matemáticos en los que se inspiraron. Por ejemplo, una computadora Int puede desbordarse, y una Double puede tener errores de redondeo. Es importante entender tales limitaciones cuando se traduce de matemáticas a código. Aquí es donde el matemático y renombrado experto de Haskell Andrés Löh entró en escena. Enseñó a los participantes cómo leer notación matemática, cómo los conceptos matemáticos se relacionan con Haskell y cómo traducir de uno a otro.
IOHK en Regensburg
Por ejemplo, Andrés presentó las primeras páginas de nuestra especificación formal de la blockchain (cadena de bloques) y habló a los participantes para que entendieran e implementaran esta pieza de matemáticas como un código Haskell simple (¡y correcto!), lo que condujo a preguntas interesantes y discusiones animadas: ¿Cómo representa usted al hashing y a otras primitivas criptográficas? ¿Qué nivel de detalle necesita? ¿Es más importante permanecer lo más fiel posible a las matemáticas o escribir un código eficiente? ¿Cuándo se debe sacrificar la precisión matemática por la simplicidad?
Además de sus grandes conferencias, John y Andrés también proporcionaron ejercicios prácticos desafiantes, donde los participantes pudieron aplicar inmediatamente sus conocimientos recién adquiridos sobre pruebas y especificaciones. Finalmente, hubo muchas oportunidades para discutir, hacer preguntas y socializar. Regensburg es una hermosa ciudad, fundada por los romanos hace dos mil años y declarada Patrimonio de la Humanidad por la Unesco. La ciudad ofreció a los participantes un marco perfecto para relajarse después de la formación, continuar sus discusiones mientras exploraban la arquitectura medieval o sentarse a disfrutar de una excelente comida y cerveza Bávara.
Material gráfico, Mike Beeple