Anfang des Monats haben wir den Quellcode für die Simplicity Blockchain Programmiersprache veröffentlicht. “Simplicity” ist unsere Lösung für die Probleme die entstehen, wenn man anspruchsvolle Smart Contracts in Blockchain Umgebungen programmiert.
Vor Simplicity mussten Blockchain Programmiersprachen Kompromisse eingehen; entweder zuverlässig oder ausdrucksstark. Entwickler mussten entscheiden zwischen komplexen jedoch unzuverlässigen Smart Contracts oder sehr einfachen, allerdings verlässlichen Smart Contracts. Mit Simplicity können Anwendungsentwickler endlich raffinierte Smart Contracts entwickeln und gleichzeitig sicher sein, dass die Ergebnisse wie erwartet zustande kommen.
Simplicity wurdeentwickelt mit Blockstreams Elements platform kompatibel zu sein. Das heißt, Entwickler die Sidechains oder unabhängige Blockchains auf Elements implementieren möchten können sehr bald alle Vorteile, die Simplicity anbietet ausnutzen. Da es um eine Implementierung von Elements handelt, wird das Liquid Netzwerk auch Simplicity unterstützen. Hiermit werden viele neue Anwendungen für Liquid Nutzern möglich sein, wie z.B. trust-minimized Hinterlegung, Tresore und andere komplexe Smart Contracts.
Neue Quellcode Features dieses Monat beinhalten:
- Denotational Semantics der Core Simplicity Sprache und Erweiterungen in Simplicity die im Coq formal überprüft werden können.
- Operational Semantics der Core Simplicity Programmiersprache, die in Coq formal überprüft werden können.
- Ein Interpreter, Type-Checker und Serialisieren der Simplicity Sprache, geschrieben in Haskell.
- Beispiel-Simplicity-Formulierungen, wie kryptographische Operationen wie SHA-256 und EC-Schnorr Signature Verifizierung.
- Ein detaillierter technischer Bericht von Simplicity.
Warum Simplicity?
Blockchains bieten mehrere einzigartige Herausforderungen welche herkömmliche Programmiersprachen ungeeignet machen.
- Alle Nutzer müssen sich auf eine Berechnung in allen Umgebungen einigen.
- Jeder Teilnehmer eines Smart Contracts sollte von allen möglichen Ergebnissen aller möglichen Eingaben im Vorfeld Bescheid wissen.
- Alle Nutzer müssen sich gegen Denial of Service Attacken wehren, die möglicherweise extrem hohen Speicherverbrauch oder Rechenzeit verursachen können.
- Jeder Teilnehmer eines Smart Contracts sollte im Voraus wissen, wieviele Kosten zu verrechnen sind für alle möglichen Eingaben.
Existierende Programmiersprachen, die bereits für Blockchains entwickelt worden sind wie z.B Ethereums EVM, müssen noch diese Herausforderungen bewältigen. Vor kurzem hat sich ein EVM upgrade beim Testing als ungeeignet erwiesen, weil sich die Implementierungen nicht mit dem berechneten Ergebnis einigen konnten. Gelder wurden bereits gestohlen oder nicht rückgewinnbar gemacht, durch logische Fehler in Smart Contracts oder Programme die ihre Maximalgrenze für die Ressourcennutzung überschreiten.
Bitcoins Skriptsprache ist wiederum zum Großteil auf eine Kombination von “digital signature checks” timelocks und hashlocks limitiert. Beeindruckende Protokolle wie das Lightning Network sind bereits auf diese Grundlagen aufgebaut, jedoch fehlt Bitcoins Skriptsprache eine Ausdruckskraft, die bei der Entwicklung von komplexen Smart Contracts erforderlich ist.
Simplicity hat das Ziel, Flexibilität und Ausdruckskraft die für Berechnungen notwendig sind, bereitzustellen, ohne auf die Sicherheit und Kosten zu verzichten, die bei der Entwicklung von Smart Contracts vorkommen.
Was ist Simplicity?
Simplicity ist eine Low Level Programmiersprache für Blockchain basierte Smart Contracts. Es wurde von Grund auf entwickelt, um einfache semantische Eigenschaften zu zeigen, was wiederum zu statische Analysen und formale Methoden führt. Die Simplicity Programmiersprache ist durch die Coq proof assistant Implementation definiert.
Die Kernsprache könnte auf einem T-Shirt angegeben werden, jedoch bedeutet Einfachheit bei der Sprache nicht Einfachheit bei der Entwicklung. Dafür gibt es einige Gründe:
- Blockchains benötigen einen grundverschiedenen Programmieransatz im Vergleich zu herkömmlicher Programmierung. Das Ziel einer Blockchain ist die Verifizierung von Berechnungen, nicht das Ausführen von Berechnungen. Das ist ein feiner, jedoch extrem wichtiger Unterschied, weil die Verifizierung bei der willkürlichen Ausführung von Code ohne Turing-Vollständigkeit möglich ist.
- Einmal ausgeführt, wird ein Smart Contract unveränderlich; somit können keine Fehler mehr behoben werden. Simplicity erkennt dieses Problem und bietet Anwendungsentwickler die Möglichkeit, formale Beweise für Smart Contracts zu kreieren.
- Simplicity ist eine Low Level Programmiersprache für eine direkte Ausführung wie die Assembler Programmiersprache und nicht wie Java oder Python. In Zukunft werden Programmierer ihre Smart Contracts in höheren Programmiersprachen entwickeln und letztendlich in Simplicity kompilieren lassen.
Was ist neu?
Nach unserem letzten Simplicity Blogeintrag waren wir sehr bemüht, von der experimentellen Sprachforschung zur formellen Sprachspezifikation zu wechseln.
Wir haben die Simplicity Programmiersprache in Coq proof assistant nachimplementiert:
- Wir haben denotationelle Semantik für die Simplicity Programmiersprache, dabei werden Erweiterungen von Witness Data, Assertions und Delegation ermöglicht.
- Eine formale Spezifikation einer abstrakten Maschine, auch “the Bit Machine” genannt, basiert auf “free categories” und ermöglicht Operational Semantics für die Simplicity Kern-Programmiersprache.
- Eine Haskell Implementierung, die in einem tagless final style entwickelt worden ist, bietet die Möglichkeit, Experimente mit Evaluierungen, Ausführungen und Type-Checking mit Ausdrücken in Simplicity auszuführen.
- Ein modularer Ansatz zu Simplicity Programmierspracherweiterungen ermöglicht es die Nebeneffekte von Spracherweiterungen zu ignorieren wenn man sie nicht benötigt.
- Wir haben viele Simplicity Ausdrücke für kryptographische Primitive, auch die von uns entwickelte Neu-Implementierung von ibsecp256k1 in Simplicity eingeführt.
- Ein technischer Bericht beschreibt eine informelle mathematische Spezifizierung der Simplicity Programmiersprache, und stellt Informationen zu Coq und Haskell Entwicklungen zur Verfügung.
Die Entwicklung von Simplicity wird ständig weiterentwickelt, jedoch können Entwickler zum ersten Mal die Simplicity Programmiersprache selber erforschen. Deshalb ist es jetzt höchste Zeit die Weiterentwicklung von Simplicity zu veröffentlichen und eine Mailingliste zu verwenden.
Wie geht’s weiter
In Zukunft gibt es viele Möglichkeiten, Simplicity weiterzuentwickeln.
Unsererseits planen wir:
- Den C Interpreter zu vollständigen.
- Implementierung einer Softwarebibliothek von JETs, die gemeinsame kryptographische Funktionen unterstützt.
- Die Verwendung von Verifiable C, um Festzustellen, dass unser C Interpreter und JETs korrekt sind.
- Simplicity in die Elements blockchain platform zu integrieren.
Unter anderem gibt es auch andere Entwicklungen:
- Die Entwicklung von Simplicity Code-Optimierungen
- Kreieren und Adaptieren von existierenden höheren Smart Contract Plattformen wie Ivy, die Simplicity generieren kann.
- Die funktionale Korrektheit von Simplicitys kryptographische Primitive mit formal correctness of cryptographic protocols zu kombinieren, damit vollständig verifizierte Smart Contracts entwickelt werden können.
Wir hoffen, dass Sie sich unserem Projekt anschließen werden.