🇪🇸 Runtime verification | Actualización Mensual Cardano | IOHK 3 Dic 2020

:es: Transcripción al español de un fragmento de “December 3rd Cardano monthly update”

Del minuto 00:26:40 al 00:47:40 del video original

Publicado en el canal de Youtube de IOHK el 3 de Diciembre de 2020

Enlace a la versión doblada al español


Tim: Bien, mira estas Devnets, se están desarrollando en asociación con un par de compañeros diferentes, uno de los cuales todos conocieron antes, otro que probablemente no. Así que primero vayamos a un clip que hice con Runtime Verification a principios de esta semana, para escuchar un poco más sobre IELE y también el trabajo que están haciendo en KEVM. Estamos muy emocionados de que se nos unan Grigore y Everett al show de Runtime Verification, antes de cavar un poco en el proyecto en sí mismo, tal vez escuchar un poco más acerca de la historia de Runtime Verification, Grigore tal vez comenzar por vos.

Grigore: Hola, gracias por invitarnos Tim y Aparna, yo empecé esta empresa Runtime Verification hace unos 10 años, el objetivo era traer al mundo real la investigación que habíamos hecho en mi laboratorio en la Universidad de Illinois, Urbana Champaign. En particular para transformar el marco K que se utilizaba principalmente para proyectos de investigación académica en un marco que pueda impulsar productos reales para clientes reales. El término mismo Runtime Verification lo acuñé creo que hace unos 15 años, cuando estaba en la Nasa, cuando se nos ocurrió este enfoque en algún lugar entre las pruebas y la verificación formal, y no sabíamos exactamente cómo llamarlo, nuestros documentos fueron rechazados tanto por la comunidad de testeos como por la de verificación formal, porque no era claramente verificación formal o testeo. Pero encontramos un terreno intermedio muy fructífero, que llamamos Runtime Verification donde parece que puedes tomar los beneficios tanto de la verificación formal como de los testeos de una manera muy práctica y llamamos a esto Runtime Verification, fue muy inspirador, inspiró una gran comunidad de investigadores, hay una conferencia internacional llamada Runtime Verification, formamos la compañía Runtime Verification y aquí estamos.

Everett: Soy Everett y me uní a la compañía a principios de 2018, originalmente era un estudiante de la UCl, en realidad en un laboratorio diferente al que dirige Grigore, y los eventos de la vida me sacaron de la universidad, y tuve que conseguir un trabajo, conseguí trabajo en Runtime Verification porque creía en lo que que estaban haciendo en términos de la semántica formal de los lenguajes de programación siendo la base de todas las herramientas que desarrollas para esos lenguajes de programación. Y cuando empecé en la empresa, el principal objetivo de la compañía eran las industrias automotriz y aeroespacial, y como dijo Grigore, en este tipo de sabor de testeo de las cosas, pero en la universidad habíamos hecho un proyecto de clase, sólo experimentando en blockchain con Ethereum y la EVM. Una vez que despegó la compañía empezamos a ver mucha demanda para hacer verificación formal, una verificación formal completa, no este tipo de mezcla entre el testeo y verificación formal de contratos inteligentes. Vimos que era comercialmente viable para hacerlo debido a que los contratos inteligentes suelen ser bastante pequeños y simples básicamente. Eso como que despegó nuestro lado del negocio de contratos inteligentes, inicialmente no estábamos realmente seguros de dónde encajábamos en el ecosistema, pero seguimos haciendo verificación formal para la gente y más recientemente hemos estado desarrollando productos, que esperamos que la gente se beneficie de ellos, en términos de mejorar la calidad de su propio código ellos mismos, sin tener que consultarnos. Recientemente estamos viendo muchas más solicitudes de auditoría de contratos inteligentes para varias aplicaciones DeFi, se siente como si hubieran pasado dos largos años o tres años en este punto, pero no sé, supongo que fue bastante rápido.

Aparna: Es una historia increíble, empezando en el espacio automotriz y aeroespacial, esos también son parte de mis antecedentes, estoy bastante familiarizada con la cantidad de testeos y el rigor que ocurre en esas industrias, y luego llevar eso a blockchain creo que es un nicho de mercado, es muy necesario, especialmente debido a hacia dónde nos dirigimos y Cardano, el proyecto en sí mismo, depende tanto de la alta calidad del código, cómo estamos testeando y cómo estamos verificando que tiene perfecto sentido que estemos trabajando juntos. Mencionaste algo sobre el espacio de contratos inteligentes y los requisitos DeFi que están recibiendo de auditorías, así que en ese sentido, desde una perspectiva de mercado, ¿hay alguna tendencia particular que te gustaría compartir con nuestra audiencia, en relación con los mercados de contratos inteligentes, a dónde ves que va y luego si no te importa Grigore después de eso me encantaría escuchar tu opinión sobre ello también?

Everett: Cuando comenzamos un montón del trabajo que estábamos haciendo era infraestructura, así que era muy básico, como una billetera multi firma, este tipo de cosas, realmente trabajo de infraestructura de bajo nivel, verificando cosas y luego hubo una especie de varias locuras cripto que han sucedido y en esos puntos normalmente se ven como un montón de contratos inteligentes de juguete, como por diversión, se hacen demasiado grandes, mucho más grandes de lo que estaban destinados a ser inicialmente. Pero más recientemente, en los últimos meses, hemos visto muchos más de estos contratos inteligentes estilo DeFi donde la gente está portando instrumentos financieros tradicionales básicamente a blockchain, tienes el mismo tipo de instrumentos financieros tradicionales, pero ahora están corriendo en blockchain de forma automatizada, y están empezando a añadir algunos giros que tal vez no aparecieron en el sector financiero tradicional. Así que creo que estamos empezando a realmente entrar en un tipo de aplicación más seria de blockchain de lo que hemos visto en los últimos dos años, donde la gente está realmente diciendo “hey, esto es real, nosotros podemos hacer realmente finanzas descentralizadas sin bancos que lo moderen”, y eso es lo que estamos viendo más en los últimos meses, son más solicitudes de auditoría para este estilo de aplicaciones, que no son sólo como plataformas de trading de crypto kitties, son instrumentos financieros reales que estamos viendo aquí.

Grigore: Me gustaría añadir que, en mi opinión, para que DeFi tenga el impacto y la enorme naturaleza transformadora que puede tener para convertirse en realidad para todos nosotros, necesitamos que entren grandes proveedores de liquidez y proporcionar grandes cantidades de dinero para que se puedan hacer grandes préstamos y que toda la infraestructura realmente reemplace el actual sistema bancario como lo conocemos. Pero para que eso ocurra, los grandes proveedores de liquidez deben confiar en este código, en estos protocolos DeFi, y hay tantas cosas que pueden salir mal ahí. Es sólo cuando se hace verificación formal del código que te das cuenta cuántas cosas pueden salir mal. Muchos entusiastas son entusiastas, piensan “oh, esto debería funcionar, es bonito”, piensan cinco segundos, diez segundos, “esto es realmente genial, hagámoslo”. Pero la realidad es que hay tantos errores ocultos, tantas posibles explosiones ahí, que las vimos con verificación formal, que es lo mejor que conocemos, es una comunidad, lo mejor que hemos hecho en 50 años más o menos de investigación, para evitar, incluso eliminar a veces, los errores de codificación. Sin eso no atraerás grandes proveedores de liquidez para intervenir, porque hay un gran riesgo, para perder a lo grande. Por eso somos firmes creyentes en el poder de verificación formal en DeFi, y creemos que en cinco años más o menos, no habrá protocolos DeFi que sean tomados en serio sin ser formalmente verificados, rigurosamente, por prestigiosos equipos. Ahora ves muchos protocolos DeFi, estos días, que son anónimos, ¿por qué son anónimos?, Sushi Swap, Panke Swap, Pickle, nadie quiere responsabilizarse por ellos, saben que podría haber bichos, podrían estar en problemas. No creo que eso tenga un futuro a largo plazo, creo que necesitan ser hechos por empresas de renombre, como Runtime Verification o tal vez Cardano o muchas otras compañías como esas y tener métodos de razonamiento poderosos detrás para analizar tanto los modelos económicos como validar propiedades importantes sobre los modelos económicos. También asegurarse que no haya errores en todo el código que pueden ser explotados.

Tim: Vamos a excavar un poco en el proyecto IELE y KEVM con el que vamos a trabajar con ustedes específicamente, pero antes tal vez volvamos al marco K y escuchar un poco más sobre ese tipo de meta que se sienta sobre estos dos y cómo eso encaja.

Grigore: El marco K es lo que llamamos un lenguaje de programación de marco semántico. Significa que formalizas matemáticamente, de forma rigurosa, tu lenguaje de programación, una vez, y luego de ese artefacto matemático derivas automáticamente o semi automáticamente todas las herramientas que necesitas para ese lenguaje como analizadores, interpretadores, compiladores, verificadores de programas, chequeadores de modelos, todas las herramientas que necesitamos para que el lenguaje pueda ser derivado en un estilo de codificación por construcción desde la definición matemática del lenguaje de programación. No hay nada que probar sobre ellos, nada que pruebe que son correctos porque se generan correctamente por construcción. Así que esa fue la firme creencia que creo que mi consejero inoculó en mi cabeza probablemente a finales de los 90, cuando me convenció de que esa es la única manera de hacerlo si queremos hacer las cosas de la manera correcta, y me enamoré de ello y después no tuve ninguna motivación para hacer las cosas de otra manera. y por eso quiero decir herramientas necesarias. Es seleccionar un lenguaje, digamos Java 4, y luego elegir una herramienta, digamos un chequeador de modelo y ahora vamos a hacer un chequeador de modelo para Java 4, pasas años trabajando en eso. Y luego, nada de eso es reutilizable para la próxima versión de Java, o C, o Solidity, o Java Script. Y eso no tenía sentido porque era como, en el mejor de los casos, un enorme desperdicio de talento y no era económico. Así que decidimos dar un paso atrás y hacer las cosas correctamente, por cierto mi consejero fue Goguen, que también es como llaman a su próxima liberación en Cardano, estoy muy honrado por ello. Así que Goguen me convenció de que si hacemos las cosas matemáticamente, rigurosamente, a largo plazo y luego diseñamos el marco K en ese espíritu, donde defines un lenguaje de programación una sola vez y luego todas las herramientas se derivan de esa única definición. Una vez que piensas sobre ello y una vez que asimilas este concepto, entonces es difícil motivarte a ti mismo para hacer las cosas de otra manera. Hemos hecho K durante muchos años, creo que empezamos a finales del 2000, en 2005 tuvimos el primer prototipo y lo tuvimos en el entorno académico, en la universidad, y luego en 2015 estaba listo para la transición a la compañía, a Runtime Verification. En 2015 empezamos a utilizar K en Runtime Verification, y teníamos la primera regla basada en él y luego otra y luego empezamos a trabajar con IOHK y las cosas crecieron desde ahí.

Aparna: En términos de las herramientas de las que estamos hablando, específicamente sobre IELE, IELE y también los productos KEVM, así que ¿por qué muchachos no me dan un poco de visión general de esos dos, cómo esto toma el marco K y a dónde ven que esto evoluciona?

Everett: Claro, te daré un poco de historia. Inicialmente KEVM comenzó como un proyecto de clase en la universidad de Illinois y entonces en realidad IOHK intervino y ellos como que vieron el futuro en la garantía de calidad de los contratos inteligentes, en el momento no estábamos pensando en hacer nada con él, era sólo un proyecto de clase en el que estábamos diciendo “bien, esto fue genial, fue un buen experimento y fuimos capaces de hacer algunas verificaciones simples y algunos testeos utilizando la KEVM”. Pero IOHK la vio y ellos se dieron cuenta de lo que significaba en términos de proporcionar garantía de calidad a un contrato inteligente y se acercaron a nosotros y dijeron “oye, ¿te gustaría convertir esto en algo más como una empresa comercial?”. Y eso es lo que realmente resultó en que fuera transferido al lado de las cosas de Runtime Verification en lugar del lado de la universidad de Illinois. Así que Runtime Verification despegó y había mucho desarrollo de infraestructura que tuvo que ocurrir inicialmente, que fue financiado en gran parte por IOHK, y luego una vez que este trabajo de infraestructura estuvo hecho, empezamos a ser capaces de ser autosuficientes básicamente en términos de hacer auditorías de seguridad de contratos inteligentes y otros modelajes de protocolos y cosas así. Así que resulta que había un enorme mercado para este trabajo de garantía de alta calidad que podríamos hacer por la gente. Así que KEVM en este punto básicamente está hecho, cuando hay una actualización, una bifurcación dura para Ethereum nosotros tenemos que hacer un pequeño trabajo de mantenimiento en ella y de vez en cuando encontramos algunas cuestiones e ineficiencias en ella y arreglamos eso. El futuro de KEVM es construyendo herramientas a su alrededor en este punto, y las herramientas que hemos hecho hasta ahora, empezamos sólo haciendo verificación formal, así que sólo teníamos herramientas de verificación formal a su alrededor, y han habido algunas otras compañías que también han construido sus propias herramientas a su alrededor, así que lo que me viene a la mente es Daphub que desarrolló el K-Lab y el lenguaje de especificación Act para hacer verificación formal más fácil utilizando KEVM, es una especie de historias de mayor éxito. Más recientemente hemos estado desarrollando esta herramienta llamada Fire Fly que somos nosotros tratando de envolver todo lo que es automatizable sobre nuestra tubería de control de calidad en una herramienta que los desarrolladores pueden conectar en su actual pila de garantía de calidad. El poder de K y KEVM viene de que tienes que conseguirlo, tienes que acceder a ella, tienes que ser un experto en métodos formales, tienes que realmente saber lo que estás haciendo. Pero hay algunas cosas más pequeñas que se pueden hacer de forma automatizada por las computadoras, así que estamos tratando de envolver todas esas pequeñas cosas en una herramienta que las personas pueden utilizar por ellos mismos, aumentar la garantía de calidad de su contrato inteligente, eso es para KEVM. IELE también comenzó hace un tiempo, fue cuando estábamos haciendo los compromisos iniciales con IOHK en 2018 y había una nueva blockchain saliendo, Cardano, y queríamos un mejor diseño de VM para ella porque luchamos mucho tratando de verificar algunos de los contratos inteligentes Ethereum iniciales utilizando KEVM porque hay un montón de, supongo decisiones de diseño extravagantes en la EVM en sí misma. Y pensamos que podíamos hacerlo mejor, así que ayudamos a Cardano a diseñar esta nueva VM llamada IELE que es mucho más influenciada por un registro base VM más moderno que la EVM. Si lees el código IELE y antes has leído el código LLVM verás que hay algunas similitudes entre los dos. Y nos beneficiamos mucho de la experiencia de la universidad de Illinois en LLVM y la escritura del compilador y toda su experiencia ahí. Así que sí, IELE en realidad comenzó como un lenguaje de diseño y lo diseñamos para que fuera más fácil de hacer razonamiento con él que EVM, sabiendo todos los problemas que tuvimos haciendo la verificación formal de EVM. IELE ahora necesita ser actualizado y por eso estamos trabajando en su actualización para llegar al punto de un estado estable como con la KEVM, y luego una vez que estemos ahí será el mismo tipo de historia, para desarrollar herramientas alrededor. Uno de los planes de cuatro a seis meses que tenemos es aplicar Fire Fly a IELE por ejemplo, y tener esta bolsa de herramientas automatizadas que los desarrolladores de contratos inteligentes que apuntan a IELE pueden utilizar, para hacer su garantía de calidad de contratos inteligentes, así que esa es como la historia de los dos.

Tim: Mencionaste que comenzamos a trabajar juntos en 2018 y obviamente desde entonces la plataforma ha recorrido un largo camino, y creo que particularmente la comunidad también ha recorrido un largo camino, así que particularmente, ¿qué te emociona e interesa acerca de trabajar con Cardano en los próximos meses?

Grigore: Puedo decirte lo que realmente me gusta sobre Cardano en general, me gusta mucho el equipo, es un equipo increíblemente fuerte, cuando miras al equipo en la página web de IOHK, casi se siente como un laboratorio de investigación de primera categoría, con los mejores investigadores, los mejores documentos, un montón de documentos publicados. Todo deriva de investigación fundamental y de entendimiento fundamental de problemas muy difíciles, así que el equipo es un factor principal para nosotros. Luego, la visión y la planificación a largo plazo también se hace de una manera que lo hace escalar. Si miras a muchas blockchains tienen esta increíble recompensa de staking como del 100 por ciento, 50 por ciento, está claro que sólo quieren hacer cosas rápidamente para atraer a masas de entusiastas, pero si miras cómo Cardano hace cada paso a lo largo de la línea muy rigurosamente, está claro que apunta al largo plazo y así es cómo hacemos las cosas en investigación fundamental, así que todo está alimentado por la investigación y realmente me gusta eso. Y particularmente me gusta el hecho de que el director general de la compañía, Charles Hoskinson, es un gran creyente del poder de la investigación y de la comprensión fundamental de las cosas, en lugar de hacer cosas particulares rápidamente. Así que eso es lo que me atrae, no sé Everett, podrías tener una mirada diferente, pero cuando pienso en Cardano eso es lo que me viene a la mente y por eso me gusta trabajar con Cardano, y soy muy optimista sobre cualquier futuro que podamos tener juntos.

Everett: Sí, mi impresión de Cardano ha sido similar, de hecho estoy impresionado con cuánto énfasis se pone en la investigación, que creo que es importante para este espacio, porque esto es nuevo, mucho de esto es totalmente nuevo, el mundo no ha visto mucho de este concepto de DeFi donde no tienes gente centralizada manejando el dinero, es totalmente nuevo. Así que creo que tiene que haber alguna investigación en términos de okay, “¿cómo vamos a hacer esto de una manera que funciona?”, y creo que Cardano está poniendo tiempo en eso y entienden la importancia de hacer eso, de hecho están acercándose a diferentes grupos de investigación, como nuestro grupo y hemos estado en contacto con algunos de los otros grupos con los que hablaron y diciéndoles “hey, nos gustaría sacar una herramienta de ti, también nos gustaría obtener un poco de investigación de ti y entender un poco más de lo que estamos tratando de hacer aquí”. Así que creo que eso es un aspecto importante de cómo Cardano está acercándose a estos problemas, en lugar del tipo de disparo de escopeta, vamos a intentar todo y ver qué se pega a la pared y quizás pierdas algo de dinero en algunos de los contratos porque no funcionó o algo así, Están tomando un enfoque mucho más de principios.

Tim: Bien, así que se avecinan tiempos muy emocionantes, muchas gracias Everett y Grigore, estamos deseando trabajar con ustedes de nuevo y más estrechamente en los próximos meses, gracias a ambos.

Aparna: Así que Tim, lo que realmente me gusta del enfoque de Runtime Verification es que están viendo esto como un tipo de concepto de universalidad, desarrolladores que desarrollan en múltiples lenguajes diferentes y cómo verifican ese código de una manera que es algo casi estándar, y la semántica K sus soluciones de la semántica K realmente lo hace muy emocionante para mí, porque simplifica muchos de los lenguajes más complejos en nuestro espacio. Así que es muy emocionante hablar con ellos, asociarse con ellos y ver a dónde vamos a ir

1 Like