A principios de este mes, lanzamos el código fuente del lenguaje de blockchain Simplicity.
Simplicity es nuestra respuesta a los problemas que enfrentamos a la hora de codificar contratos inteligentes_ _sofisticados en ambientes de blockchain. Antes de Simplicity, los https://docs.google.com/document/d/1Eibvv2w5oNWKGFfExkYCznQcxz-j2–RzVnSgsIU_J0/edit?usp=sharinglenguajes de programación de blockchain normalmente tenían que encontrar un punto medio entre la expresividad y la confiabilidad; los desarrolladores tenían dos opciones: crear un contrato inteligente complejo pero poco confiable o uno muy básico pero seguro. Con Simplicity, los desarrolladores por fin pueden diseñar contratos inteligentes** **sofisticados y confiar en los resultados.
Simplicity fue desarrollado para que sea compatible con la plataforma de Elements de Blockstream. Eso significa que los desarrolladores que diseñen sidechains o blockchains independientes en Elements pronto podrán aprovechar las funciones que habilita Simplicity. Al ser una implementación de Elements, Liquid Network también será compatible con Simplicity, lo cual ofrecerá aplicaciones interesantes a los usuarios de Liquid, tales como contratos de garantía en los que se minimice la dependencia en la confianza, cajas fuerte y otros contratos inteligentes más complejos.
La fuente lanzada este mes incluye:
- La semántica denotativa del núcleo del lenguaje de Simplicity y sus extensiones, detalladas formalmente en Coq.
- La semántica operativa del núcleo del lenguaje de Simplicity, detallada formalmente en Coq.
- Un intérprete, un corrector de escritura y la serialización del lenguaje de Simplicity disponibles en Haskell.
- Ejemplos de expresiones de Simplicity, incluidas algunas operaciones criptográficas, tales como el SHA-256 y la verificación de firmas EC-Schnorr.
- Un informe técnico en el que se detalla el lenguaje de Simplicity.
¿Por qué Simplicity?
Los blockchains presentan diversos desafíos únicos que hacen que los lenguajes de programación tradicionales sean inadecuados.
- Todos los usuarios deben estar de acuerdo sobre el resultado de una computación en todos los entornos.
- Todas las partes de un contrato inteligente deben conocer por adelantado todos los posibles resultados de todas las posibles entradas al programa.
- Todos los usuarios deben ser capaces de evitar ataques de denegación de acceso, que consumen exceso de memoria o tiempo de computación.
- Todas las partes de un contrato inteligente deben comprender desde el principio los costos de ejecución del programa para todas las posibles entradas.
Los lenguajes de programación disponibles diseñados específicamente para blockchains, tales como EVM de Ethereum, aún se enfrentan a estos desafíos. Recientemente, una actualización de EVM falló durante las pruebas porque las implementaciones no concordaban en el resultado de una computación. Se han robado o perdido irrevocablemente fondos debido a errores de lógica en contratos inteligentes y a programas que superan los límites de sus recursos.
Por otro lado, el lenguaje Script de Bitcoin suele estar limitado a combinaciones de verificaciones de firmas digitales, timelocks y hashlocks. Si bien hay algunos protocolos notables (como por ejemplo Lightning Network) que se desarrollaron en base a estas primitivas, el lenguaje Script de Bitcoin no cuenta con la expresividad necesaria para crear contratos inteligentes más complejos.
Simplicity apunta a brindar flexibilidad y expresividad para cualquier computación que el usuario necesite, al tiempo que permite verificar la seguridad y los costos de los contratos inteligentes.
¿Qué es Simplicity?
Simplicity es un lenguaje de programación de bajo nivel y un modelo de máquina para contratos inteligentes basados en blockchain. Fue diseñado desde cero con el fin de que tenga una semántica simple, que facilite el análisis estático y el razonamiento por métodos formales. El lenguaje de Simplicity está definido a partir de su implementación en el proof assistant de Coq.
Si bien el núcleo del lenguaje es tan simple que cabe en una camiseta, la simpleza de un lenguaje no es sinónimo de simpleza en el desarrollo. Esto es así por varios motivos:
- Los blockchains involucran un modelo de programación fundamentalmente diferente de la programación ordinaria. La función de un blockchain es verificar la computación, en vez de llevar a cabo la computación. Es una distinción sutil, pero sumamente importante ya que es posible verificar la ejecución de códigos arbitrarios, sin la necesidad de que sea un sistema Turing completo.
- Una vez formado, el contrato inteligente es inmutable y no deja margen para corregir errores. Simplicity aborda ese problema ya que permite a los usuarios crear pruebas de corrección formales para los contratos inteligentes.
- Simplicity es un lenguaje de nivel extremadamente bajo para ejecución directa, más similar al lenguaje de ensamblador que a Java o Python. En última instancia, esperamos que los usuarios puedan redactar sus contratos en uno o más lenguajes de nivel más alto, que luego se compilarían con Simplicity.
¿Cuáles son las novedades?
Desde nuestra última entrada sobre Simplicity, trabajamos arduamente para avanzar de la investigación de un lenguaje experimental a una especificación de lenguaje más formal.
Reimplementamos el lenguaje de Simplicity en el proof assistant de Coq:
- Contamos con semántica denotativa para todo el lenguaje de Simplicity, incluidas las extensiones de lenguaje que respaldan los witness data, las aserciones y la delegación.
- Una especificación formal de una máquina abstracta llamada “the Bit Machine” basada en categorías libres brinda la semántica operativa para el núcleo del lenguaje de Simplicity.
- Una implementación Haskell desarrollada en base al tagless final style permite al usuario experimentar con la evaluación, la ejecución y la corrección de escritura de las expresiones de Simplicity.
- Un enfoque modular a las extensiones del lenguaje de Simplicity permite al usuario ignorar los efecto de las extensiones del lenguaje si no las está utilizando.
- Tenemos una gran variedad de expresiones de Simplicity para primitivas criptográficas, incluida nuestra reimplementación de libsecp256k1 en Simplicity.
- Un informe técnico que brinda una especificación matemática informal del lenguaje de Simplicity y presenta las guías para los desarrollo Coq y Haskell.
Si bien el desarrollo de Simplicity aún no ha concluido, llegamos a un punto en el que los desarrolladores pueden explorar por sí solos el lenguaje de Simplicity. Por lo tanto, llegó la hora de abrir el desarrollo de Simplicity y crear una lista de correos.
Próximas novedades
A futuro, son muchas las direcciones en las que puede desarrollarse Simplicity.
Nuestro plan consiste en:
- completar el intérprete C.
- implementar una biblioteca de jets para diversas funciones criptográficas comunes.
- utilizar el Verifiable C para demostrar que el intérprete C y los jets son correctos.
- integrar Simplicity con la plataforma de blockchain de Elements.
Otros frentes de desarrollo incluyen:
- el desarrollo de optimizadores de código de Simplicity.
- la creación de nuevas (o adaptar existentes) plataformas de contratos inteligentes de alto nivel, tales como Ivy, para generar Simplicity.
- combinar la corrección funcional de las primitivas criptográficas de Simplicity con la corrección formal de los protocolos criptográficos para crear contratos inteligentes completamente verificados.
Esperamos que nos decida acompañar en nuestro proyecto.