Una deliberación y descripción de cómo Tauchain trabaja escrito por un no experto.

Aviso:

En primer lugar, voy a decir que no me considero un experto en el tema de Tauchain, o en el tema de la programación funcional. Mi experiencia se basa en la seguridad de la información y la filosofía (ética). Mis conocimientos teóricos sobre estos temas provienen de mi formación académica, años de investigación personal y discusiones con el desarrollador de Tauchain Ohad Asor. Para una descripción más precisa más allá de lo que ofrezco remitase por favor a Ohad Asor.

¿Qué es Tauchain?

Muchos programadores experimentados, licenciados en ciencias de la computación, expertos en criptografía, tienen dificultades en entender exactamente lo que es Tauchain y por qué es tan importante. El propósito de lo que estoy haciendo aquí es ayudar a desmitificar y elucidar la forma en que Tauchain está actualmente planeado para funcionar. Estaré deliberando temas como la lógica y sus implicaciones para la seguridad de la información en el software. Estaré deliberando cómo se prueba el software y por qué el lenguaje imperativo completo de Turing representa un riesgo para todos los contratos inteligentes que intentan ser confiables. Voy a hablar de Notación3 con algunos ejemplos sobre cómo la programación en Tau puede funcionar y mucho más.

El diseño es algo importante y Tauchain está bien diseñado

Una de las razones por las que me interesé en Tauchain es que me di cuenta de que los desarrolladores detrás de él estaban dispuestos a crear algo que podríamos llamar arte. Yo mismo leo muchas revistas académicas y reconozco cuando los desarrolladores están haciendo investigaciones serias. En mi primera comunicación con Ohad me preguntó acerca de la Teoría tipo Martin Lof y de la cual hasta ese momento nunca había oído hablar. No sabía quién era Martin Lof o por qué era importante, pero como investigador diligente seguí todo lo que Ohad dijo y llegué a la conclusión de que Martin Lof es uno de los lógicos más importantes de nuestro tiempo. La Teoría tipo Martin Lof es extremadamente importante y me di cuenta de que Teoría tipo Martin Lof y estaba ligeramente relacionada con algo que tropezó en mi propia investigación llamada lógica intuicionista. La lógica intuicionista introduce el concepto de la prueba constructivista que en términos básicos significa que demuestras por ejemplo (prueba demostrativa) más que por la representación simbólica sola.

Una breve explicación de la lógica proposicional para explicar el poder de los contratos inteligentes decidibles.

Para entender lo que Tauchain puede hacer es posible que necesite entender los fundamentos básicos de la lógica. Si usted es un filósofo puede estar familiarizado con la lógica, pero para aquellos que no tienen antecedentes filosóficos daré una explicación sencilla sobre lógica proposicional.

Los fundamentos básicos de la lógica proposicional requieren una comprensión de las conexiones lógicas. Los programadores de ordenadores tienen un concepto similar llamado operadores lógicos como el “si”, “y”, “o” con lo que es más fácil de entender.

• Conjunción significa “y”.
• Disyunción significa “o”.
• Negación significa “no”.
• Implicación significa “si … entonces”.
• Equivalencia significa “si y sólo si”.
• Negación alternativa significa “no ambos”

T =Verdadero, F = Falso

Además de estas descripciones en español, también hay símbolos. Los símbolos principales utilizados en una tabla de verdad de lógica proposicional son P y Q. Voy a dar un breve ejemplo de cómo se usa.

En una tabla de verdad hay 4 operaciones unitarias.

Siempre verdadero.
Nunca verdadero.
Operación nularia
Operación nularia negativa

En la tabla de la verdad.

Un argumento lógico requiere una premisa y una conclusión. Una tabla de verdad tiene T o F donde cada sentencia en la tabla debe ser verdadera o falsa (T o F).

Para cada declaración distinta utilizamos la letra P o Q.

P: Barack Obama nació en los Estados Unidos.
P: Barack Obama es el Presidente de los Estados Unidos en 2016.

P y Q: T (es cierto que Barack Obama es Presidente de los Estados Unidos en 2016) + (es cierto que Barack Obama nació en Estados Unidos).
(P∧Q)

Barack Obama es el Presidente de los Estados Unidos en 2016 sólo si Barack Obama nació en los Estados Unidos.

Solo si Barack Obama nació en los Estados Unidos puede Barack Obama ser Presidente de los Estados Unidos en 2016.

Etiquetar la primera sentencia P como A.
Etiquetar la segunda sentencia Q como B.

B ==> A

La segunda afirmación que es verdad implica que la primera declaración debe ser verdadera. De hecho, la segunda afirmación sólo puede ser verdadera si la primera afirmación es verdadera.

De este modo si tenemos una tabla de verdad se pueden tomar hechos basados en lo que se sabe que es verdadero o falso, y siguiendo las reglas de la lógica derivan en una conclusión de T o F. Debido a que siempre se puede derivar una conclusión de T o F a cualquier Declaración que mantenga la coherencia lógica. Es esta consistencia lógica la que permite un cómputo decidible, pero con el fin de conseguir que se pierda la integridad. Es por esta razón que el Turing completo es indeseable si desea confiar en la seguridad basada en el nivel de lenguaje basado en lógica. La seguridad del nivel de lenguaje basado en lógica toma la forma de carga del programador al tener que preocuparse de que la programación sea segura o realizar una programación defensiva porque el propio lenguaje es defensivo y la seguridad se obtiene por coherencia lógica. Simplemente no es posible que haya una contradicción lógica, así que si volvemos al ejemplo de Obama simplemente no es posible que P sea falso y Q sea verdad, pero B implica A. Barack Obama es el Presidente de los Estados Unidos solamente Si Barack Obama nació en los Estados Unidos de lo contrario tendrás una contradicción lógica que hace que todo careza de sentido.

El Turing completo permite este tipo de contradicciones. En lugar de sí o no, verdadero o falso, se obtiene sí y no, verdadero y falso, que son salidas sin sentido. Esto hace que el cálculo no termine nunca. Sigue en el infinito porque el Turing completo va con la idea de que hay infinita memoria y tiempo infinito. Todo el conocimiento actual del universo revela exactamente lo contrario y muestra que tienes una energía finita que no puede ser creada o destruida. Esto también implica que la información no puede ser creada o destruida incluyendo la información que cae en un agujero negro y escapa en forma de radiación. La teoría incompleta de Gódel demuestra que el universo no permite tanto la integridad como la consistencia que revela algo acerca de la naturaleza del universo, así como los límites de lo que es computable.

La importancia del isomorfismo de Curry Howard revela que los programas son pruebas

Y si los programas son pruebas entonces los contratos inteligentes son pruebas porque los contratos inteligentes son programas. Las pruebas lógicas son el núcleo de todos los programas y los programas decidibles son pruebas lógicamente consistentes. Esto es algo para recordar para entender por qué Tauchain se basa en reglas y cómo funciona. También explica algo fundamental sobre cómo Tauchain puede ser capaz de crear reglas, conocimientos, pruebas, porque las reglas se basan enteramente en la lógica, el conocimiento es lo que se demuestra en verdad, las pruebas son posiblemente demostrativas (pruebas constructivistas). Cuando compaginas todo esto, tienes la trilogía en el libro blanco de Ohad donde la lógica permite la derivación correcta de la prueba de sus axiomas / hipótesis / premisa.

Paradigma de la computación/programación blanda (soft coding / Soft computing):

Computación blanda (Soft computing):

Al mirar los contratos inteligentes o software en general, tenemos dos paradigmas diferentes. La computación blanda es un paradigma en el que se consideran aceptables las aproximaciones, imprecisiones y soluciones inexactas a tareas computacionalmente duras. Un ejemplo de soft computing es usar un algoritmo genético para evolucionar una solución o si queremos ver Maidsafe / SAFE Network para ver que está usando una solución de computación blanda donde no tienes una estructura de datos blockchain en absoluto y en su lugar tienes un Algoritmo tipo colonia de hormigas modificado. La cadena de bloques de Bitcoin también es parte del paradigma de computación blanda porque no hay una solución óptima posible para el problema de los generales Bizantinos (Byzantine generals). Esto se debe a que el teorema CAP muestra que es lógicamente imposible tener más de dos fuera mediante la consistencia, disponibilidad y tolerancia de la partición. En la fase de investigación ayuda a entender lo que es imposible antes de comenzar el desarrollo. Satoshi Nakamoto se basa en la minería NP dura, y el consenso distribuido eso es un problema que ningún algoritmo puede resolver eficientemente. Maidsafe y Satoshi Nakamoto se basan en el enfoque de la informática blanda para resolver el problema porque no existe un algoritmo que pueda dar una solución precisa.

Codificación blanda (Softcoding):

La codificación blanda es un patrón de diseño mucho más seguro y más inteligente. Cualquier valor comúnmente alterado debe ser codificado con software. La codificación blanda promueve la libertad y la personalización. El software que es codificado de este modo es más fácil de realizar los deseos del usuario. Tau lleva esto al extremo donde la red Tauchain es completamente autodefinida. Es auto-poético en el sentido de que una vez que esté completamente configurado y particularmente funcionando con Agoras será autorganizado y también autonomo en el mantenimiento. Tauchain será lo que los primeros usuarios quieren que sea. Tauchain es lo más flexible posible, lo cual es bueno para la libertad.

Paradigma de la Computación/programación dura (hard computing / hard coding)

Computación dura (Hardcomputing):

Por otro lado, la computación dura puede contribuir a la sobre-ingeniería porque algunos problemas no pueden resolverse a través de la computación dura, porque ninguna solución eficiente puede existir. El análisis de decisiones, la agregación de preferencias y la toma de decisiones son problemas difíciles de NP en el sentido de que no se puede confiar en el algoritmo perfecto o que sea exacta cualquier tipo de computación dura. En esencia, sólo se pueden resolver este tipo de problemas con soft computing, lo que significa que pueden utilizar blockchains, inteligencia de enjambre, votar, todo lo que es el soft computing. Tau específicamente evitó esto pasando a la estructura de datos de la cadena de bloques (tauchain) y mediante la autodefinición de sus reglas.

Códificación dura (Hardcoding):

La codificación dura es un antipatrón común. La codificación dura permite y contribuye a que el programador cometa muchos errores. Tauchain comienza sin ninguna regla en absoluto en el contexto de la raíz que significa que no es hardcoded en absoluto. Los primeros usuarios tendrán lo que parece ser una flexibilidad ilimitada para definir Tauchain. Esto significa que Tauchain potencialmente puede mantener siempre la alineación con el interés propio de la comunidad que establece sus reglas y en los casos en los que la comunidad puede estar en desacuerdo no hay bifurcaciones. En lugar de hacer un fork sería muy simple, crear simplemente un nuevo contexto y un nuevo derivado del cual todo el mundo obtiene lo que quiere mediante la separación del contexto. El problema de Bitcoin o de Ethereum decidiendo fork o no fork se haría irrelevante en Tauchain.

Una breve introducción al lenguaje de programación Notation3

Notation 3 se basa en el concepto de sujeto -> predicado -> objeto. Es único en su simplicidad pero es lo suficientemente poderoso para describir cualquier cosa. La Notation 3 permite al programador convertirse en un ingeniero de ontología y describir por sujeto -> predicado -> objeto, es mejor si lo describo como un gráfico lógico.

Cómo es en Tau

Comencemos con una oración en español: Alicia conoce a Bob.
El sujeto es Alicia.
El predicado es conoce.
El objeto es Bob.

En este caso, el predicado describe lo que Alice hace o es. Sabe que es algo que Alicia puede hacer porque es un ser humano y un humano tiene esa capacidad. Bob es un humano también y puede conocer a Alicia. Esto revela que hay una lógica en el fondo que discutiremos más adelante pero primero echemos una ojeada al código.

Ejemplo en Notation3 codigo siguiente:

@prefix ppl: <http://ejemplo.org/gente#>.
@prefix foaf: <http://xmlns.com/foaf/0.1/>.

ppl:Alicia foaf:conoce ppl:Bob

El código anterior utiliza el @prefix de manera similar a cómo C o C++ usa encabezados o Python utiliza la importación. Se denomina declaración de espacio de nombres y, aunque no es necesario, puede facilitar la escritura en Notation3. Notation3 también tiene vocabularios y reglas.

Ejemplo de una regla a continuación:

@prefix ppl: <http://ejemplo.org/gente#>.
@prefix foaf: <http://xmlns.com/foaf/0.1/>.

{
    ppl:Alicia foaf:conoce ppl:Bob.
}
=>
{
    ppl:Bob foaf:conoce ppl:Alicia.
}.

¿Recuerdan la lógica proposicional? La lógica es la base de las reglas en la Notation3.

El "=>" significa implica. Si esto entonces esto. Expresado sucintamente, afirma que sí Alicia conoce a Bob entonces Bob conoce a Alicia.

Para decirlo de otra manera, que Alicia conozca a Bob implica que Bob conozca a Alicia. Esto se convierte en una regla y una vez que la conviertes en una regla en Notation3, puedes razonar basándote en ese conocimiento de reglas. Tau tendrá un razonador que puede aplicar el razonamiento deductivo automáticamente para deducir hechos adicionales al gráfico del conocimiento. Por ejemplo, si Tau sabe lo que es un ser humano y sabe que todas las personas son humanas y todos los seres humanos son mamíferos, entonces puede darse cuenta de que Alicia y Bob son mamíferos si son humanos usando el razonamiento deductivo. Esto es muy potente para los programadores si se usa adecuadamente.

Como se puede ver los conceptos básicos de Notation3 no son difíciles y si bien es una comprensión básica de la lógica puede que no sea muy diferente de la lógica que la gente espera obtener con condicionales en los lenguajes de programación tradicionales. Lo que es diferente es que nosotros tenemos un razonamiento automatizado. Nosotros describimos cómo debe funcionar un programa en lugar de decirlo a través de comandos paso a paso. A medida que Tau crezca, su base de conocimientos crecerá y podrá consultar a Tau para recopilar fragmentos de código. Seremos capaces de saber exactamente lo que va a hacer y la programación se hará más fácil con el tiempo.

Cuando tratamos con un software que no es decidible hay maneras de tratar de hacer algo confiable. Todos los métodos conocidos comúnmente se basan en pruebas de caja negra. Se llama prueba de caja de bloqueo porque primero tenemos que reconocer que no podemos saber con certeza lo que pasa en la caja negra. Sólo podemos trabajar para tener cuidado con nuestra entrada y analizar la salida.

Cuando se trata de una caja negra, se trata de una lógica indecidible. Cuando se trata de una caja negra se trata de una situación en la que es posible que pueda experimentar comportamientos inesperados que pueden dar lugar a consecuencias no deseadas para los participantes en el contrato inteligente. Con el fin de crear un contrato inteligente seguro utilizando un lenguaje completo de Turing se tiene que ser extremadamente cuidadoso para defenderse contra las entradas elaboradas mientras que al mismo tiempo se tiene que analizar las salidas. Puede tomar muchos años de pruebas antes de obtener un software que funcione como usted piensa que debe funcionar a menos que pueda averiguar lo que pasa en la caja negra.

¿Por qué pueden ser imposibles los contratos inteligentes confiables en Ethereum y una elección entre la fiabilidad y la inmutabilidad puede ser inevitable?

Actualmente, los contratos inteligentes de Ethereum no son fiables. Muchos investigadores en seguridad y personas altamente competentes dicen que a un nivel fundamental estos contratos inteligentes nunca serán confiables. En mi opinión, si bien es posible crear contratos inteligentes confiables, no es posible hacerlo de forma coherente con las herramientas actuales y se necesitaría una reelaboración completa de Ethereum para abordar esta situación mediante la puesta en práctica de una verificación formal mínima obligatoria que aun así todavía podría no garantizar la producción de contratos inteligentes perfectamente confiables, pero sería mejor que ahora.

El problema con Ethereum se deriva del hecho de que requiere que los contratos inteligentes sean confiables para ser valioso del todo. Es una plataforma valiosa basada en el hecho de que ofrece lo que la gente espera que sean los contratos inteligentes confiables. Es valioso basado en el hecho de que la gente espera que porque Ethereum es descentralizado que será más confiable y más seguro que centralizado. El hack DAO expone el hecho de que los contratos inteligentes no son confiables y tal vez en realidad no es más seguro que la web centralizada.

La inmutabilidad es una característica deseada porque la gente quiere saber que los contratos inteligentes potencialmente vivirán para siempre. Tengo que decir que la inmutabilidad es un ideal similar que no funcionará en la práctica al igual que el Turing completo requiere que no tenga consistencia, el hecho es que con Ethereum puede ser deseable tener inmutabilidad pero la inmutabilidad sin confiabilidad es inútil.

Si hay contratos inteligentes que son a su vez poco fiables e inmutables, entonces se obtendrá lo peor de dicha combinación. Tienes la inseguridad y también obtienes algo peligroso que sería un contrato inteligente que no puede ser cerrado incluso cuando la mayoría del planeta piensa que debería serlo. Por esta razón, Ethereum probablemente tendrá que sacrificar la inmutabilidad para una fiabilidad satisfactoria. La fiabilidad satisfactoria significa que si hay un error en un contrato inteligente, entonces puede haber un proceso de hard fork y restaurar los fondos o si hay una confiscación injusta que se pueda deshacer y restaurar.

Tauchain es hasta ahora la única plataforma que garantiza contratos inteligentes confiables

Tauchain puede garantizar la fiabilidad de los contratos inteligentes debido a los métodos formales utilizados, el lenguaje de programación totalmente funcional dependiendo del lenguaje de programación escrito, los Agoras que podrán comprar computación, almacenamiento e incluso código en sí, a partir de un mercado inteligente. Si va a haber un contrato inteligente de mil millones de dólares es probable que nunca vaya a estar en Ethereum y más que probable que estará en Tauchain o en un sucesor.

Esto no significa que nada pueda salir mal con Tauchain. Va a ser un desafío extremo incluso para crear Tauchain y Tau el lenguaje de programación puede tomar años antes de que la gente pueda entender el valor. Por último, no menos importante es posible que la gente lo vea como una moda en lugar de que es confiable y en este caso, podemos tener un futuro donde la gente almacena miles de millones de dólares en contratos inteligentes con errores de los que se aprovecharan ida y vuelta los hackers, la esperanza es Tauchain que ofrece la alternativa para las personas que se preocupan por los contratos inteligentes de misión crítica y experimentos serios que requieren una garantía de fiabilidad.

Post original de Dana Edwards en Inglés con permiso del autor para su traducción al español: A discussion and description of how Tauchain works by a non-expert