# Comprender la decidibilidad de Clarity ### ¿Qué significa que un lenguaje sea no completo de Turing o decidible? Los términos no completo de Turing y decidible son dos expresiones que a menudo escucharás sobre las ventajas de seguridad de Clarity, pero ¿qué significan? Aunque están relacionados, no son del todo intercambiables, ya que existen algunas diferencias. #### No completo de Turing Un sistema o lenguaje es no completo de Turing si no puede simular una máquina de Turing, que es un modelo abstracto de computación. Los sistemas no completos de Turing tienen una capacidad computacional limitada en comparación con los sistemas completos de Turing. Un sistema o lenguaje completo de Turing puede simular cualquier máquina de Turing. Entre los ejemplos de sistemas no completos de Turing se incluyen las máquinas de estado finito y algunos lenguajes específicos de dominio (como Clarity). Los lenguajes no completos de Turing por lo general no pueden expresar todos los algoritmos posibles. En concreto, algunos problemas cuyas soluciones requieren bucles o recursión ilimitados no pueden expresarse usando lenguajes no completos de Turing. Esta última propiedad es especialmente importante en el contexto de Clarity, ya que hace que características como los bucles ilimitados y la reentrancia estén prohibidas a nivel del lenguaje. #### Decidible Un problema es decidible si existe un algoritmo que siempre puede determinar si una entrada dada tiene o no una propiedad particular en una cantidad finita de tiempo. En otras palabras, un problema decidible puede ser resuelto por una máquina de Turing que tiene garantizado detenerse para todas las instancias de entrada. La decidibilidad es una propiedad de los problemas, mientras que la completitud de Turing es una propiedad de los lenguajes o sistemas computacionales. El hecho de que Clarity sea decidible significa que los desarrolladores (y las herramientas) pueden razonar más fácilmente sobre el comportamiento de los contratos de Clarity y predecirlo con certeza, independientemente de la entrada. ### Mentalidad de un desarrollador de contratos inteligentes Antes de entrar en detalles, primero establezcamos el contexto y la perspectiva que debemos adoptar como desarrolladores de contratos inteligentes que quieren escribir código seguro. A medida que explores más a fondo las propiedades de seguridad de Solidity y Clarity, verás que siempre hay medidas de mitigación que *pueden* ser tomadas por los desarrolladores para ayudar a abordar algunos de estos problemas de seguridad. El principal problema de esta línea de pensamiento es que aumenta la probabilidad de error humano en la seguridad de los contratos inteligentes. Si podemos preservar la funcionalidad al mismo tiempo que mitigamos al máximo la posibilidad de error humano, debemos hacerlo. ### ¿Deberían los contratos inteligentes ser completos de Turing? Descubriremos nuevas aplicaciones para los contratos inteligentes. Estas aplicaciones irán más allá de los contratos inteligentes actuales y de los contratos tradicionales, e incluso podrían abrir nuevas oportunidades económicas. Dadas estas posibilidades, ¿cómo deberíamos construir nuestros contratos inteligentes? ¿Qué características deberían tener nuestros lenguajes de contratos inteligentes? Es una buena práctica separar los datos de los programas. ¿Deberían los contratos inteligentes ser datos, o programas, o algo intermedio? Si los contratos inteligentes son datos, entonces ¿los programas que los ejecutan deberían ser completos de Turing o quizás menos potentes? Si los contratos inteligentes son programas, entonces ¿en qué lenguaje deberían escribirse? ¿Qué características debería tener este lenguaje de programación? La tesis de Church–Turing es la hipótesis de que todas las nociones formales de computación quedan capturadas por las máquinas de Turing o las computadoras modernas. Un lenguaje de programación es completo de Turing si captura todas las nociones formales de computación. Muchos lenguajes de programación son completos de Turing. Por ejemplo, Python, C++, Rust, Java, Lisp y Solidity son todos completos de Turing. Considera un programa y su entrada. En el peor de los casos, determinar la salida de este programa es imposible. La validación de un programa, para una entrada concreta, se hace generando una prueba de corrección. Las pruebas de corrección son pruebas lógicas que pueden verificarse mecánicamente. Encontrar pruebas de corrección para programas y su entrada es indecidible. Kurt Gödel demostró que existen enunciados lógicos indecidibles. Esto indica que todos los programas en lenguajes completos de Turing no pueden validarse en el peor de los casos. Por lo tanto, los lenguajes de contratos inteligentes completos de Turing deben permitir contratos que no puedan validarse. Alonzo Church y Alan Turing demostraron que existen problemas que son incalculables. Los problemas incalculables no pueden ser resueltos por ninguna máquina de Turing. Por lo tanto, asumiendo la tesis de Church–Turing, estos problemas incalculables no pueden ser resueltos por ninguna computadora. Exploraremos esta idea más adelante en esta sección. Los lenguajes completos de Turing son muy expresivos. De hecho, asumiendo la tesis de Church–Turing, los lenguajes completos de Turing son, en cierto sentido, tan expresivos como es posible. ¿Existe una compensación? ¿Qué tipos de problemas pueden surgir con problemas incalculables y programas cuya validez puede ser indecidible? A medida que los contratos inteligentes absorben partes del derecho contractual, considera el amplio conjunto de leyes y regulaciones del derecho fiscal. Por ejemplo, la legislación y la normativa fiscal de EE. UU. ocupan varios millones de palabras. La legislación y la normativa fiscal internacional elevan mucho más estas cifras. ¿Estas leyes y regulaciones son programas o son datos? Si el derecho fiscal se escribiera en un lenguaje completo de Turing, entonces la ley podría codificar problemas incalculables. Para un contable sería una pesadilla que su asesoramiento fuera indecidible. Clarity no es completo de Turing, pero sí muy expresivo. Esto hace que Clarity sea decidible y que no pueda codificar problemas incalculables. Hay debates y artículos sobre lenguajes de contratos inteligentes como Solidity que proponen subconjuntos de Solidity que no son completos de Turing. Estos subconjuntos son decidibles y no pueden codificar problemas incalculables. Sin embargo, no hay consenso sobre qué subconjuntos utilizar y no se usan ampliamente. ### Ventajas de la decidibilidad en los contratos inteligentes ¿Por qué es importante la decidibilidad en el contexto de los contratos inteligentes? En primer lugar, no es posible que una llamada de Clarity se quede sin gas en mitad de una ejecución. Debido a su decidibilidad, es posible obtener un análisis estático completo del grafo de llamadas para tener una imagen precisa del costo antes de la ejecución. Solidity permite bucles ilimitados, recursión y llamadas dinámicas a funciones, lo que dificulta predecir con precisión de antemano el costo de ejecución o el uso de gas. Como resultado, los contratos de Solidity pueden quedarse sin gas durante la ejecución si el límite de gas no se establece adecuadamente o si el contrato encuentra un escenario con requisitos computacionales inesperadamente altos. Un ejemplo práctico es el problema de un tipo específico de ataque DoS en Solidity, en el que el contrato queda inutilizable debido a restricciones de ejecución ilimitadas. Un ejemplo de esto es el ataque GovernMental, donde un mapeo que debía eliminarse para un pago se volvió tan grande que trabajar con él superó el límite de gas del bloque. Hay varias propiedades distintas del diseño del lenguaje de Clarity que impiden este tipo de ataques DoS. La razón por la que el sistema de análisis puede estimar con precisión el costo de ejecución es porque cierta funcionalidad está intencionalmente limitada en Clarity. Por ejemplo, no hay recursión en Clarity, así que no podemos llamar indefinidamente a una función una y otra vez. Los tipos de datos en Clarity también están restringidos. Cualquier tipo de dato que no requiera un límite de longitud fijo no es iterable. Los mapas y las tuplas, por ejemplo, no requieren que se introduzca una longitud máxima al definirlos, pero tampoco se pueden iterar. Las listas, en cambio, que sí son iterables, requieren que el desarrollador defina un límite superior al definirlas. Esto es una gran parte de lo que permite un análisis estático preciso de los contratos de Clarity. Entonces, ¿cómo implementaríamos un mapeo de tamaño indefinido en Clarity? No lo haríamos, porque es un antipatrón en el diseño de contratos inteligentes. En su lugar, Clarity nos obliga a pensar en una mejor solución para nuestro problema. Por ejemplo, implementar una forma para que los usuarios gestionen por sí mismos las operaciones sobre elementos de mapeo/lista, en lugar de operaciones masivas gestionadas a nivel del contrato. Si [analizas el ataque GovernMental](https://hackernoon.com/smart-contract-attacks-part-2-ponzi-games-gone-wrong-d5a8b1a98dd8#h-attack-2-call-stack-attack), verás que aprovechó múltiples problemas de seguridad, todos ellos mitigados en Clarity. También verás que se añadió una corrección para hacer económicamente inviable volver a realizar este tipo de ataque. Esto plantea otro punto crucial al establecer modelos mentales apropiados para los contratos inteligentes y los sistemas blockchain: más complejidad significa más posibles errores, lo que significa añadir aún más complejidad para abordar esos errores. Cuando esto ocurre una y otra vez, nos estamos atrapando en la creación de un sistema cada vez más complejo. Abordar estos problemas a nivel del lenguaje evita esta complejidad en constante crecimiento. Para profundizar en cómo se diseñó Clarity, consulta [SIP-002](https://github.com/stacksgov/sips/blob/main/sips/sip-002/sip-002-smart-contract-language.md). {% hint style="info" %} Puedes ver algunas vulnerabilidades más comunes de los contratos inteligentes y cómo se mitigan en [este artículo](https://stacks.org/bringing-clarity-to-8-dangerous-smart-contract-vulnerabilities/). {% endhint %} Esto también tiene efectos de segundo orden cuando analizamos las pruebas de seguridad y las auditorías. Una de las herramientas comunes para probar contratos inteligentes es la verificación formal, donde demostramos matemáticamente que ciertas propiedades de los contratos inteligentes seguirán siendo verdaderas o no en todos los casos. Esto puede conducir al problema de la explosión de caminos, donde hay tantos caminos disponibles que la verificación formal se vuelve increíblemente difícil. Este problema se mitiga en Clarity, ya que no hay posibilidad de que un programa se encuentre con un bucle ilimitado. Esto nos lleva a un modelo mental más general para pensar en la decidibilidad a medida que los contratos inteligentes siguen convirtiéndose en una parte más grande de nuestra economía. Recuerda que el objetivo de los sistemas blockchain es crear un sistema financiero abierto, transparente y justo. Esto significa que los contratos inteligentes serán responsables de gestionar grandes cantidades de riqueza para un número cada vez mayor de personas. A medida que los contratos inteligentes abarquen más estructuras financieras, su complejidad y uso crecerán. La complejidad es enemiga de la seguridad. Cuanto más complejo es un sistema, mayor es el peligro de crear problemas incalculables cuando no hay restricciones estrictas sobre los pasos de ejecución que pueden tomarse. Esto es letal en una infraestructura financiera que no solo es abierta y transparente, sino inmutable. Exploremos un poco más esta idea de incalculabilidad. ### Intuición sobre la incalculabilidad De forma intuitiva, la incalculabilidad es una visión algorítmica de la indecidibilidad. La incalculabilidad tiene los mismos fundamentos que la indecidibilidad. Las preguntas indecidibles se formulan como enunciados lógicos o enunciados sobre enteros. Por supuesto, los programas son enunciados lógicos e incluso pueden considerarse enteros, aunque los vemos de forma diferente. A menudo vemos los programas con detalles adicionales de modelos de memoria, detalles de implementación y semántica de ejecución. El [problema de la parada](https://en.wikipedia.org/wiki/Halting_problem): Como ejemplo, dado cualquier programa `P` y cualquier entrada finita `I` para `P`, entonces el problema de la parada es el reto de determinar si `P` se detiene con la entrada `I`. Alonzo Church y Alan Turing demostraron que el problema de la parada es irresoluble. Christopher Strachey dio una prueba intuitiva por contradicción que muestra que el problema de la parada es incalculable. Esto se plantea suponiendo que existe un programa `H` que puede resolver el problema de la parada para cualquier programa `P`. `H(P)` devuelve verdadero si `P` se detiene y falso en caso contrario. Luego se construye un programa `P` que no se detiene cuando `H(P)` es verdadero, dando lugar a una contradicción. Del mismo modo, este programa `P` se detiene cuando `H(P)` es falso, lo que también es una contradicción. Los problemas incalculables son problemas que no pueden resolverse mediante un algoritmo o una computadora, sin importar cuánto tiempo o recursos se proporcionen. Estos problemas existen en varias formas, y un ejemplo de ellos es el problema de correspondencia de Post, propuesto por Emil Post. El problema de correspondencia de Post puede describirse usando pares de cadenas y un entero. Imagina que tienes n pares de cadenas, llamados P. Estas cadenas están formadas por caracteres de un conjunto de caracteres, como UTF-8 o cualquier otro alfabeto con al menos dos símbolos. Los pares de cadenas se ven así: ``` P = { (x1, y1), (x2, y2), … , (xn, yn) } ``` Ahora, también tienes un entero m mayor que 0. El problema de correspondencia de Post pregunta si existe una forma de crear una lista de índices (i1, i2, …, im) usando los pares de cadenas dados. Puedes repetir estos índices si es necesario, con una condición: cuando combinas las cadenas x de los pares usando los índices, la cadena resultante debe ser igual a las cadenas y combinadas de los mismos pares usando los mismos índices. En otras palabras: ``` x(i1) x(i2) … x(im) = y(i1) y(i2) … y(im) ``` Cuando los desarrolladores intentan resolver el problema de correspondencia de Post, a menudo intentan usar bucles indeterminados (bucles sin un número fijo de iteraciones) en lugar de recursión. Esto se debe a que el problema parece requerir explorar diferentes combinaciones de índices hasta que se encuentre una solución o se demuestre que no existe ninguna. En términos simples, el problema de correspondencia de Post consiste en intentar encontrar una secuencia de índices que, al aplicarse a los pares de cadenas dados, produzca cadenas concatenadas iguales tanto a partir de los componentes x como de los y. Este problema se considera incalculable porque no existe un algoritmo general que pueda resolverlo para todos los posibles pares de entrada de cadenas y enteros. Resulta que muchas preguntas sobre cómo se comportan los programas son incalculables. Esto tiene una serie de consecuencias para los contratos inteligentes construidos en lenguajes completos de Turing, muchas de las cuales aún no conocemos pero de las que sin duda seremos conscientes a medida que las encontremos en el futuro. ### La intuición de Raymond Smullyan sobre la indecidibilidad Esta es una parte del enfoque de Raymond Smullyan para entender la indecidibilidad en la lógica proposicional. Utiliza metainformación para mostrar que algo debe ser verdadero, aunque no pueda probarse en la lógica proposicional. Esto se basa en una paradoja. En lógica proposicional, un enunciado lógico es indecidible si no podemos demostrar que es verdadero o falso. Dado un enunciado de lógica proposicional S, una prueba es una secuencia de deducciones lógicas formales, que comienza con hechos básicos y termina indicando si S es verdadero o falso. Smullyan comienza con una isla de caballeros y bribones. Los caballeros siempre dicen la verdad. Los bribones siempre mienten. No podemos distinguir a los isleños por otro medio. Hay un gran lógico llamado Ray. Todo lo que Ray demuestra es verdadero. Es como un buen demostrador de teoremas. Un isleño llamado Jack le proclama al lógico Ray: “No puedes demostrar que soy un caballero”. El siguiente razonamiento se basa en el metaconocimiento de esta situación. Este metaconocimiento muestra que algunos problemas son indecidibles en lógica proposicional. Si Ray puede demostrar que Jack es un caballero, entonces Jack debe ser un bribón, ya que Jack debió haber mentido. Eso es porque Ray demostró que Jack es un caballero. Como Jack es un bribón, la prueba de Ray contradice la suposición de que Ray solo demuestra cosas verdaderas. Por lo tanto, este caso no puede sostenerse. Si Ray no puede demostrar que Jack es un caballero, entonces Jack debe ser un caballero, ya que Jack dijo la verdad. Pero Ray no puede demostrar el hecho de que Jack es un caballero. En el contexto de los contratos inteligentes y los lenguajes de programación, los lenguajes completos de Turing como Solidity vienen con la posibilidad de problemas indecidibles. Estos problemas indecidibles son similares a la paradoja presentada en la historia de los caballeros y bribones, donde es imposible determinar si Jack es un caballero o un bribón basándose en la información dada. En la historia de los caballeros y bribones, Ray es análogo a un demostrador de teoremas o a un contrato inteligente en un lenguaje completo de Turing. Ray se enfrenta a un enunciado que es indecidible dentro de las restricciones del sistema (caballeros y bribones), lo que conduce a una paradoja. De manera similar, un lenguaje de contratos inteligentes completo de Turing podría enfrentarse a problemas indecidibles que no pueden resolverse, lo que daría lugar a comportamientos inesperados, vulnerabilidades o problemas de consumo de recursos (como quedarse sin gas en Ethereum). Por otro lado, los lenguajes no completos de Turing como Clarity están diseñados para evitar problemas indecidibles limitando su expresividad. En el contexto de la historia de los caballeros y bribones, un lenguaje no completo de Turing simplemente no permitiría que Jack hiciera una afirmación que pudiera llevar a una paradoja. Al prohibir ciertas características como los bucles ilimitados y la recursión, los lenguajes no completos de Turing pueden ofrecer garantías más fuertes sobre el comportamiento y el uso de recursos de los contratos inteligentes. Esta previsibilidad es deseable en muchos casos, especialmente cuando se trata de transacciones de alto valor o sistemas críticos. ### Referencia The Mathematics of Various Entertaining Subjects: Research in Recreational Math Illustrated Edition, Jennifer Beineke (Editor), Jason Rosenhouse (Editor), Raymond M. Smullyan (Foreword), Princeton University Press, 2016.