Tezos è formalizzato o è definito dal comportamento di un programma?
Le regole del protocollo Bitcoin sono definite dal comportamento dell'ultima versione di Bitcoin Core, mentre Ethereum è definito dal contenuto dello Yellow Paper.
Come viene definito il corretto comportamento della blockchain di Tezos?
Risposte
Il protocollo Tezos è definito dalla sua implementazione OCaml. Quando viene proposto un emendamento al protocollo, i delegati votano sugli hash delle implementazioni modificate.
Detto questo, alcune parti del protocollo sono state formalizzate. In particolare, la semantica del linguaggio del contratto intelligente di Michelson è stata formalizzata in diversi framework semantici: Coq , Ott , K e Why3 . Per altre parti, come la procedura di modifica e l'algoritmo di consenso, la formalizzazione è in corso e, per quanto ne so, i documenti più dettagliati che abbiamo sono quelli della sezione "whitedoc" dihttps://tezos.gitlab.io.