🇪🇸 Fusionar los métodos formales y el desarrollo ágil para construir Cardano

:es: Traducción al español de “Merging formal methods and agile development to build Cardano

Publicado por Philipp Kant en el blog de IOHK el 9 de Abril de 2020


El director de métodos formales de IOHK, Philipp Kant, expone nuestra metodología para construir software con flexibilidad y precisión

Forma y función

IOHK está construyendo Cardano en un sistema operativo financiero y social global. Esta enorme tarea requiere tanto una rápida iteración como una precisión absoluta. Es por eso que IOHK ha elegido combinar la velocidad del desarrollo ágil con un código de alta seguridad y métodos formales. La fusión de la flexibilidad y la formalidad llevó a nuestros ingenieros a ser pioneros en esta moderna filosofía de desarrollo.

IOHK cree firmemente en la investigación, los métodos formales, la programación funcional y la construcción de manera rigurosa. Como competidor en la industria del desarrollo blockchain, también tenemos que demostrar consistentemente el progreso y crear valor para nuestra comunidad global de interesados. Esto significa que no podemos comprometer la robustez o la velocidad y flexibilidad del desarrollo. En un mercado en constante cambio esto es un desafío, por lo que nuestros desarrolladores tienen que encontrar un equilibrio.

Agilidad versus formalidad

La norma inicial para el desarrollo de la tecnología ha sido construir rápidamente un producto mínimo viable y luego iterar continuamente hasta que esté listo para el mercado de masas. Esto se conoce como un proceso ágil. Es una gran manera de demostrar que un proyecto está avanzando mientras eventualmente se construye un producto completamente funcional. Sin embargo, una metodología ágil asume que habrá errores y debilidades en cada paso del desarrollo que pueden ser resueltos más tarde. Esto está bien si no hay ningún valor en riesgo - pero, con las monedas virtuales, hay una enorme cantidad de dinero y confianza de los interesados en juego.

La construcción de un activo digital en una blockchain plantea varios desafíos que hay que superar en cuanto a la organización de un proceso de desarrollo. Como prueba de la criptografía, Cardano es un sistema distribuido en un entorno adversario en el que es fundamental un rendimiento constante. El protocolo tiene que mantener la seguridad frente a los agentes malintencionados que intentan el sabotaje. Esto significa que nadie puede permitirse el lujo de construir rápidamente y tratar los problemas más tarde.

La confianza es esencial para que una moneda sea aceptada y las pruebas de corrección son una forma importante de aumentar la veracidad de un sistema. Por eso el código no sólo debe ser correcto, sino que debe haber pruebas de su corrección, tales como extensas pruebas significativas y pruebas matemáticas. En una industria joven como la de las cripomonedas, los ingenieros de IOHK tienen que anticipar la adición de nuevas características manteniendo las garantías de corrección establecidas en la versión inicial. La plataforma sólo puede escalar globalmente si es capaz de crecer manteniendo la seguridad y la utilidad para todos. Por eso los desarrolladores de Cardano racionalizaron su metodología, combinando una variedad de herramientas que van desde las pruebas basadas en propiedades hasta las pruebas verificables por máquina, para crear un software de alta garantía incluso en presencia de requisitos cambiantes.

La investigación para codificar

La metodología comienza con la investigación científica. Hasta la fecha, IOHK ha publicado más de 60 trabajos de investigación que han contribuido a la creación de la plataforma. Cada trabajo examina un aspecto crítico de la tecnología blockchain desde los primeros principios. ¿Cómo se logra el consenso de manera descentralizada? ¿Cómo se diseña un contrato inteligente? ¿Cuál es la estructura de recompensa adecuada para incentivar el buen comportamiento? Los investigadores de IOHK examinan estas preguntas y envían sus respuestas a revistas científicas y conferencias. Estos trabajos contienen pruebas que deben pasar por una rigurosa revisión por pares. Luego, para asegurar que la calidad de nuestro software haga justicia a la ciencia, se desarrolla usando métodos formales.

En esencia, esto significa que los ingenieros de IOHK especifican lo que el código debe hacer matemáticamente. De esa manera, pueden asegurarse de que cuando el código se ejecute, contenga las propiedades deseadas diseñadas en él. El código está escrito en Haskell, un lenguaje de programación funcional de alta seguridad con un fuerte sistema de tipos. Aunque Haskell es una gran herramienta para implementar software confiable, no es infalible, por lo que el código aún debe ser probado. Una gran manera de escribir pruebas es usando QuickCheck, que permite a los desarrolladores declarar propiedades que siempre deberían estar en un programa. QuickCheck luego genera casos de prueba, y busca contra-ejemplos mínimos que violen esas propiedades.

En el código que interactúa con el mundo externo, en particular las aplicaciones de red, puede ser difícil encontrar contra-ejemplos mínimos. Esto se debe a que el orden de ejecución no es determinístico: puede cambiar cada vez que se ejecuta el software. El mismo código puede ser ejecutado cientos de veces, y sólo falla una vez. Podemos evitar esto usando simulaciones con orden de ejecución determinista. Ejecutar pruebas en la simulación nos permite encontrar y arreglar de forma fiable una clase de errores en las pruebas, que de otra forma sólo ocurrirían al azar en la producción.

Cerrar la brecha

Para tener una idea de la metodología de desarrollo empleada por Cardano, consideremos la metáfora de la construcción de puentes. Cuando un ingeniero civil construye un puente, gran parte de su tiempo lo pasa detrás de un escritorio. El ingeniero civil planea un diseño, calcula la estática y ordena estudios geográficos. Durante ese tiempo, no ocurre nada en el lugar de la construcción. Un observador no podría ver ningún progreso que se esté realizando. Para construir puentes, este es el enfoque correcto. Si la planificación no es exacta, es difícil y costoso corregir los problemas en una etapa posterior. En última instancia, el resultado sería un puente retrasado a un costo más alto, o uno que falle completamente. La falta de progreso visible es un buen precio a pagar por un puente funcional y seguro.

Cuando se construye un software, hacer cambios en etapas posteriores es mucho más fácil que en la construcción. Eso es lo que permite el enfoque de desarrollo ágil común. Si un desarrollador ágil estuviera construyendo un puente, construiría un pilar en un rápido sprint y luego el siguiente en un segundo sprint. La brecha entre los pilares se cubriría en un sprint final y, si las cosas no se sostuvieran, los desarrolladores añadirían un sprint más para arreglar cualquier problema. Mientras que el progreso sería demostrable en el sitio de construcción, el producto final probablemente tendría una gran cantidad de problemas incorporados. Esto crea un trabajo de limpieza al final del proyecto que podría haberse evitado con una mejor planificación en una etapa anterior. Además, el producto mínimo viable probablemente se entregaría a un pequeño grupo de personas para una prueba de conducción con la expectativa de que fracasara a fin de alertar a los desarrolladores de los errores. No hace falta decir que es mejor que los puentes no se diseñen de esta manera.

Al escuchar las palabras “métodos formales”, mucha gente en el desarrollo de software piensa en el enfoque de la ingeniería civil, que es apodado “cascada” y generalmente rechazado. Este es un malentendido común pero desafortunado. En efecto, el uso de técnicas formales apropiadas nos permite tener nuestro pastel, y comerlo también: tener un diseño global (un diseño deliberado, no accidental de encajar piezas desarrolladas en sprints), mostrar el progreso continuamente, y conservar la capacidad de reaccionar a los requerimientos cambiantes.

Una técnica clave empleada por los desarrolladores de IOHK son las especificaciones ejecutables. Estos son diseños de alto nivel, que abstraen sobre detalles de bajo nivel, escritos en un lenguaje que la computadora puede entender y ejecutar. Las especificaciones ejecutables pueden ser utilizadas como prototipos para mostrar el progreso, obtener retroalimentación de los usuarios y probar las suposiciones. Además, se pueden añadir detalles de nivel inferior mediante sucesivos refinamientos. Nuestros desarrolladores construyen el puente para resolver los problemas más grandes primero y luego añaden pilares para reforzarlo más tarde. En un sistema de software, los pilares serían características como guardar datos en el disco, o usar algoritmos de rendimiento, que se necesitan para un producto final, pero que no son esenciales para demostrar la funcionalidad general.

Usando especificaciones ejecutables, obtenemos los beneficios de una planificación adecuada sin sacrificar la flexibilidad. Los desarrolladores de IOHK pueden arreglar cómo debería ser el sistema a gran escala, y luego implementar los componentes adecuados según sea necesario. Las pruebas continuas garantizan que cada componente se ajuste al diseño general. Esto ayuda a prevenir problemas que son comunes en un enfoque de integración tardía. Con esta metodología, obtenemos lo mejor de ambos mundos: podemos usar un diseño de arriba hacia abajo (evitando problemas de integración tardía, teniendo un buen manejo del diseño general en todo momento), y tener el código de trabajo temprano (demostrando el progreso, y permitiendo pruebas y retroalimentación a través de todo el proceso).

A prueba de futuro

En última instancia, el método de construcción debe ser determinado por lo que se está construyendo. IOHK está construyendo un sistema operativo social y financiero global que requiere rigor y rapidez. Formal versus ágil es una falsa dicotomía. En su lugar, seguimos desarrollando nuestra metodología que fusiona lo mejor de ambos enfoques: técnicas formales dentro de un marco de entrega ágil, con un código robusto y de mayor garantía sobre el que podemos construir para todos nuestros futuros.

2 Likes