Transcripción al español de un fragmento de “Cardano 2nd Anniversary meetup - AMA with IOHK, EMURGO & Cardano Foundation”
Del minuto 21:24 al 26:50 del video original
Publicado en el canal de Youtube de IOHK el 30 de Septiembre de 2019
Ir a la versión doblada al español
Pregunta número 10 de @kernmantelseil y es para IOHK ¿Habrá una colección de contratos inteligentes probadamente seguros que uno puede seleccionar de una biblioteca y modificar? En caso afirmativo, ¿cómo una biblioteca de este tipo se realizará, curará y mantendrá segura?
Esa es un pregunta interesante, hicimos una hoy, ustedes vieron el contrato Búlgaro de fideicomiso, usamos una solución SMT ahí, que es bastante bueno, podría incluso entrar en nuestra biblioteca. Los estándares son la primera capa, tienes que tener un nivel razonable de discusión acerca de lo que estamos hablando, ¿cómo se clasifica un activo?, ¿cómo se clasifica una identidad?, ¿cómo se clasifica la información criptográfica primitiva dentro del sistema? Y esos sub-componentes tienen que ser construidos o por nosotros o alguna buena compañía y la verificación formal requiere un poco de tiempo allí, es mucho trabajo de esfuerzo, entonces una vez que tienes esos primitivos se puede componer los primitivos juntos para construir más contratos y bibliotecas sofisticadas.
Pero es una pregunta abierta, no es sólo que tenemos librerías o un SDK sino que ¿necesitamos siquiera escribir otro DSL?, como por ejemplo, averigüemos que tal vez 30% de todo el uso de Cardano termina siendo la gestión de la cadena de suministro, puede tener sentido entonces construir lenguaje de dominio específico, específicamente para las cadenas de suministro.Y con sólo hacer eso podemos sacar mucho más provecho de la herramientas para verificar que estos contratos están en lo cierto. Esa es de hecho una de las razones por las que creamos Marlowe, dijimos, bien esto es mayormente un sistema financiero, no tiene sentido tratar de implementar contratos financieros en un lenguaje de programación de propósito general, hagámoslo en un un lenguaje mucho más simple y es considerablemente más fácil hacer lo que hicimos aquí hoy, construir un contrato con alguien en una laptop, en vivo que nunca lo miró antes y verificó que ese contrato no tiene ningún problema existencial como el Dowhack, etc. Esa es una filosofía y un enfoque, tenemos un grupo de métodos formales y hemos invertido un montón de esfuerzo, tiempo y dinero en ello y ciertamente están emergiendo técnicas de métodos formales que tal vez sean más livianas y suficientemente buena para la mayoría de los desarrolladores.
Pero es importante entender que no hay magia probada detrás de estas cosas, incluso si tienes una especificación, tienes un código que has probado por simulación con el código, es tan bueno como la especificación y segundo, no te protege contra el fraude. Por ejemplo, puedo tener el mejor contrato inteligente de lotería del mundo que siempre me paga cada vez que la lotería entra, está funcionando, se supone que tiene que pagarme bien. Así que yo podría hacer eso, y así que es sólo una herramienta, un modelo de comprobar la propiedad basado en la prueba de una letanía de estas herramientas que existen. Pero se empieza con la conversación sobre las especificaciones, el estándar, ese es el número uno. Luego trabajas a través de eso y segregas las cosas que son realmente malas para todos, si te equivocas esa es la cripto, de la cosas que es una batalla personal, si te equivocas ese es tu sabor particular de esa implementación. Luego para el material que es universal, es donde se aplican las herramientas más pesadas para, por ejemplo, Microsoft está haciendo un gran trabajo con el proyecto Everest y F Star tratando de reescribir TLS para que sea formalmente verificado. Algunos proyectos incluso están utilizando esa parte del apilamiento y hay algo de mérito, es trabajo y es bueno y para ciertas partes de nuestro sistema como UTxO Accounting, por ejemplo, escribimos muy extensas especificaciones formales porque si nos equivocamos, eso es muy, muy, muy malo para todo el mundo en el ecosistema entero. Pero va a ser un esfuerzo a largo plazo para construir estas bibliotecas.
También había una pregunta acerca de la curaduría, ¿quién más va a constrúirlos?, ¿cómo los curaremos?, ¿cómo los evolucionaremos? y esa es otra interesante pregunta abierta, sería realmente interesante ver si el sistema de tesorería podría utilizarse en tándem para cuestiones de prioridades, por ejemplo la actualización de las bibliotecas. Quizás sea el caso para que tres, cuatro o cinco años en el futuro, mientras la gente construye ese pastel de dónde gastar el dinero de Cardano, que hay un grupo de personas que son expertos en métodos formales, no necesariamente IOHK, pero podría ser Gawa o alguna compañía que a menudo dicen “chico, nos encantaría ir y actualizar la biblioteca estándar que ustedes tienen para este lenguaje en particular y verificar que todo está bien, agregar muchas capacidades y funcionalidad a él”. Ok, entonces la comunidad tendrá que sentarse y la gente que está proponiendo tendrá que hacer un caso de por qué eso agregaría valor al ecosistema y probablemente esa sea una característica de gobernanza descentralizada. Así que algunos de ellos provienen de casos de uso, algunos de ellos provienen de la segregación de universales versus particulares y otros de intereses financieros y personas que hacen propuestas interesantes, es también un enfoque multi-modelo donde no se trata de probar una sola técnica de método formal, incluso en nuestra propia compañía tenemos muchas técnicas diferentes que usamos, tenemos Iteris y Agda, Cack, K, hemos escrito cosas ahora que estamos empezando en TL Plus, estamos usando Isabel para ciertos componentes, así que hay una naturaleza polígama en lo que hacemos y a cada uno de estos es sólo uno de los muchos tipos específicos de herramientas quirúrgicas para resolver problemas particulares