Ist Tezos formalisiert oder wird es durch das Verhalten eines Programms definiert?

Nov 01 2020

Die Regeln des Bitcoin-Protokolls werden durch das Verhalten der neuesten Bitcoin Core-Version definiert, während Ethereum durch den Inhalt des Gelben Papiers definiert wird.

Wie ist das korrekte Verhalten der Tezos-Blockchain definiert?

Antworten

4 RaphaëlCauderlier Nov 02 2020 at 03:50

Das Tezos-Protokoll wird durch seine OCaml-Implementierung definiert. Wenn eine Änderung des Protokolls vorgeschlagen wird, stimmen die Delegierten über Hashes geänderter Implementierungen ab.

Davon abgesehen wurden einige Teile des Protokolls formalisiert. Insbesondere wurde die Semantik der Michelson-Smart-Contract-Sprache in mehreren semantischen Rahmenbedingungen formalisiert: Coq , Ott , K und Why3 . Für andere Teile, wie das Änderungsverfahren und den Konsensalgorithmus, ist die Formalisierung noch nicht abgeschlossen, und AFAIK, die detailliertesten Dokumente, die wir haben, gehören zum Abschnitt "whitedoc" vonhttps://tezos.gitlab.io.