Enlace a la versión doblada al español
Además aquí está la transcripción completa, traducida y revisada para el Canal Cardano Castellano
Transcripción completa
Doblaje al español de “Behind the Blockchain Part III: Formalizing the Innovation Model”
Publicado en el canal de Youtube de IOHK el 18 de Octubre 2024
Mencionamos mucho que está bien, comenzamos con la investigación y los problemas, luego innovación e implementación, pero estamos dispuestos a pensar en todo esto como un ciclo o un sistema. Tenemos cosas que entran en la innovación, pero tal vez también hay cosas que regresan de la innovación a la investigación.
Necesitamos tener una pregunta de investigación primero, y la pregunta de investigación obviamente también puede provenir del lado de la ingeniería. Simplemente tenemos esta implementación con una limitación, ¿podemos superarla? ¿Puedes encontrar una manera de abordar este problema y encontrar una solución a esta cuestión específica de ingeniería que tenemos cuando debemos implementar diseño?
Cuando hablamos de todo este proceso de formalización, creo que la forma en que me gusta pensar en ello, y algo que intentamos trabajar en el equipo de Peras, fue este proceso de traducción. Piensa en el lenguaje de los artículos científicos como una cosa, y luego el lenguaje al que queremos traducir ese lenguaje a algo comprensible por una máquina. Básicamente, lo que hacemos es esta formalización en Agda, donde tienes algo que está muy cerca de lo que está en el artículo, pero verificable por una máquina, y a partir de lo cual potencialmente podrías derivar y mecanizar las pruebas. Pero también tienes todo tipo de traducciones.
Tienes esta traducción de este modelo formal a un modelo realmente ejecutable, que son cosas diferentes, porque cuando tienes que ejecutar el modelo, ya no es lo mismo que lo que mencionas, Sandro. Está bien intercambiar cadenas completas en el papel, pero en la práctica, tendrías que traducir esa idea cruda, necesitás propagar cadenas con un límite de tiempo, en algo práctico, porque no puedes pensar que vas a mover 150 GB de datos en 5 segundos. Entonces, ¿cómo haces eso? Esa es otra traducción que debemos hacer desde la formalización, que funciona y puede ser verificada por máquina, hasta un prototipo o un modelo ejecutable que puedas simular.Luego tienes una tercera capa, o un tercer o cuarto paso de traducción, que sería cómo traducir todas estas ideas en algo que sea una especificación que alguien pueda usar. Sí, lo hicimos juntos en el taller de Paris.
Quería decir que en la primera etapa que mencionaste, fui testigo de un poco de magia en ese taller de Paris, donde en un plazo de una hora aproximadamente, las personas de métodos formales presentes escribieron algo, no estoy seguro de cómo llamarlo, quizás un compilador o un intérprete, que toma el lenguaje pical que usamos en nuestros artículos para describir un protocolo, que está destinado a humanos, y lo transforma en algo que tiene un significado semántico dentro del modelo Agda.
Y creo que este paso es muy interesante y muy importante porque también queremos este tipo de modelo formal en algún momento. Quizás sea algo en lo que podamos pensar para mejorar en el futuro, haciéndolo más cercano a la forma en que trabajan los investigadores, logrando que todo este proceso de interacción sea más fluido y más regular, mucho más rápido, en lugar de tener que trabajar con grandes pedazos, hacerlo de manera más rápida.
Creo que la comunidad de criptografía en general también podría beneficiarse de esto. Muchos escriben pseudocódigo en sus artículos, pero cada uno usa un estilo de pseudocódigo ligeramente diferente. Entonces, si existiera un tipo de pseudocódigo estándar que pudiera traducirse de forma automatizada
De hecho, incluso más allá de eso, muchos artículos en nuestra comunidad tratan sobre protocolos muy complejos, y no algo tan claro y sencillo como Peras, y si eres el lector de esos artículos, a veces puede ser muy frustrante. Es molesto escribirlos, pero también es difícil leerlos y captar de inmediato las ideas; necesitas revisar muchos detalles de las pruebas. Hasta cierto punto, si esto pudiera automatizarse y realmente verificarse de manera mecánica, podrías escribir un artículo que solo transmita las ideas, pero la parte formal estaría en algún tipo de código.
O lenguaje que tenga un respaldo en el que puedas confiar, lo cual te daría el resultado formalizado con ciertas propiedades.
Creo que sería interesante escuchar lo que tienes que decir sobre esto, Nicholas, ya que existe toda esta idea de que mencionamos mucho que empezamos con la investigación y los problemas, luego pasamos a la innovación y después a la implementación, pero queremos pensar en todo esto como un ciclo o un sistema.:Tenemos elementos que avanzan hacia la innovación, pero tal vez también hay cosas que regresan de la innovación hacia la investigación.
Es básicamente volver al punto de Christian al inicio de la charla cuando estábamos hablando de que necesitamos tener una pregunta de investigación primero y la pregunta de investigación obviamente también puede provenir del lado de la ingeniería. Es decir, hemos implementado esto de cierta manera, tenemos esta limitación, o si podemos superarla, ¿podemos encontrar una forma de abordar este problema y encontrar una solución a este problema de ingeniería específico que tenemos al implementar el diseño? Así que sí, y también uno de los usos
muy útiles de la formalización es esta idea, como mencionaste, de poder ofrecer un prototipo a partir de la formalización, y es el primer paso hacia la implementación. Podemos empezar a tener un modelo de referencia que esté formalmente verificado, sobre el cual podemos comparar una implementación real, ya sea para un prototipo o para una implementación en producción. Entonces, esta formalización no es solo para asegurarnos de que tenemos ciertas propiedades; también es una forma de verificar que otros prototipos también tendrán ciertas
propiedades que nos son relevantes, y desde esta perspectiva es muy interesante.
Creo que también, anecdóticamente, es interesante también en términos de comunicación, porque se tiene como un punto central de comunicación donde se puede decir “ok, en lugar de discutir algo que es un poco informal y que está sujeto a interpretación humana, tenemos un pseudo código”. Como mencionaste, Sandro, esta idea de que cada artículo cripto usa un pseudo código ligeramente diferente, con interpretaciones ligeramente diferentes de cosas que parecen iguales pero no lo son exactamente. Hay una charla y un artículo famoso de Guy Steele sobre esto, donde menciona que analizó diez años de presentaciones en POPL y a partir de ahí observó cómo se usa un lenguaje que todos entienden y nadie usa, y el formalismo en lenguajes. Hay como 30, 40 o 50 formas diferentes de definir los mismos elementos en los lenguajes, y creo que lo mismo sucede en la cripto; todos tienen sus propias formas, incluso hay una teoría donde ves lo que se utiliza, todos tienen su propia manera
En lo personal, prefiero un enfoque en el cual, en lugar de ser extremistas de la formalización, donde todo debe formalizarse y codificarse, optamos por un enfoque en el que queremos formalizar y acordar cosas que faciliten el proceso de comunicación entre humanos. Eso es importante, no eliminar a los humanos del proceso, sino facilitar su trabajo, de manera que no tengamos que repetirnos; así, las cosas obvias para unos se hacen evidentes para todos rápidamente, sin necesidad de repetirlas o explicarlas constantemente.
También se trata de la presentación. En ciencia, es muy importante ser preciso. Claro que el texto en inglés también puede ser preciso; los filósofos lo hacen todo el tiempo. Y creo que el paso hacia la formalización es muy importante, aunque menos intuitivo. Imagina un proceso en el que una persona lee una especificación: puedes ser preciso, pero, como dijo antes Sandro, confiar en que la idea está ahí y los artefactos son verificables, permitiendo centrarse en la idea y los teoremas precisos, sabiendo que existe algo ejecutable.
El objetivo de la formalización en esta parte es lograr consistencia interna: tienes un modelo, un algoritmo, y todo es consistente. Nos encontramos con un caso curioso en un documento en el que trabajamos juntos, había un parámetro que se usaba sin estar definido, se utilizaba pero no estaba realmente definido. Si hubiera sido comprobado por máquina, no habrías podido hacer eso porque cada símbolo debe definirse en algún lugar. Es un ejemplo trivial de algo que, si se lee con atención, podría captarse, pero delegar esto a las máquinas simplifica la vida de todos y evita preguntas largas.
Y cuando eres preciso y defines que algo no completamente definido realmente significa que no está definido, y el pseudo código significa que no es código. Es una forma de ser precisos sin ser ejecutables por máquina, y el paso para llenar esta brecha es crucial.