TY - GEN

T1 - UTxO- vs Account-Based Smart Contract Blockchain Programming Paradigms

AU - Brünjes, Lars

AU - Gabbay, Murdoch J.

PY - 2020

Y1 - 2020

N2 - We implement two versions of a simple but illustrative smart contract: one in Solidity on the Ethereum blockchain platform, and one in Plutus on the Cardano platform, with annotated code excerpts and with source code attached. We get a clearer view of the Cardano programming model in particular by introducing a novel mathematical abstraction which we call Idealised EUTxO. For each version of the contract, we trace how the architectures of the underlying platforms and their mathematics affects the natural programming styles and natural classes of errors. We prove some simple but novel results about alpha-conversion and observational equivalence for Cardano, and explain why Ethereum does not have them. We conclude with a wide-ranging and detailed discussion in the light of the examples, mathematical model, and mathematical results so far.

AB - We implement two versions of a simple but illustrative smart contract: one in Solidity on the Ethereum blockchain platform, and one in Plutus on the Cardano platform, with annotated code excerpts and with source code attached. We get a clearer view of the Cardano programming model in particular by introducing a novel mathematical abstraction which we call Idealised EUTxO. For each version of the contract, we trace how the architectures of the underlying platforms and their mathematics affects the natural programming styles and natural classes of errors. We prove some simple but novel results about alpha-conversion and observational equivalence for Cardano, and explain why Ethereum does not have them. We conclude with a wide-ranging and detailed discussion in the light of the examples, mathematical model, and mathematical results so far.

UR - http://www.scopus.com/inward/record.url?scp=85096504298&partnerID=8YFLogxK

U2 - 10.1007/978-3-030-61467-6_6

DO - 10.1007/978-3-030-61467-6_6

M3 - Conference contribution

AN - SCOPUS:85096504298

SN - 9783030614669

T3 - Lecture Notes in Computer Science

SP - 73

EP - 88

BT - Leveraging Applications of Formal Methods, Verification and Validation: Applications. ISoLA 2020

A2 - Margaria, Tiziana

A2 - Steffen, Bernhard

PB - Springer

T2 - 9th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation 2020

Y2 - 20 October 2020 through 30 October 2020

ER -