64 min listen
Amrit Kumar & Dr.Ilya Sergey: Scilla – A Formal Verification Oriented Contract Language
FromEpicenter - Learn about Crypto, Blockchain, Ethereum, Bitcoin and Distributed Technologies
Amrit Kumar & Dr.Ilya Sergey: Scilla – A Formal Verification Oriented Contract Language
FromEpicenter - Learn about Crypto, Blockchain, Ethereum, Bitcoin and Distributed Technologies
ratings:
Length:
72 minutes
Released:
Jun 6, 2018
Format:
Podcast episode
Description
With the rise of smart contract technology, we’ve become acutely aware of the need for smart contract code to accurately reflect the intentions of its author; and for the code to have certain (safe) behaviors in all circumstances. Creating the languages and software tools to enable ordinary developers to write safe contracts has become an intense research endeavor in the cryptocurrency space.
Scilla is a Turing incomplete intermediate level language; inspired from the paradigms of functional programming and formal verification; that makes it easy for smart contract developers to automatically prove statements about smart contract behavior. For example, Scilla could allow a future multi-signature smart contract author to mathematically prove that funds in that contract would always be retrievable by certain addresses (and never get stuck like the Parity incident). The ability to mathematically prove such safety properties of the smart contract has the potential to be an enabling invention prior to widescale use of this technology.
In this episode, we are joined by Dr. Amrit Kumar and Dr. Ilya Sergey to discuss Scilla, the smart contract language of the upcoming Zilliqa blockchain. In a previous episode, we’ve already covered the vision and technical approach of Zilliqa to solve the transaction scalability problem of permissionless blockchains. This episode focuses specifically on their smart contract language development efforts.
Topics covered in this episode:
Updated on Zilliqa’s progress since our last episode
The technology of mechanised proofs
Dr. Ilya Serger’s effort to mechanically prove safety properties of a blockchain consensus network
Aims of the Scilla language
Future capabilities enabled by the Scilla language
Developer experience and perspective using formal verification tools
How Scilla compares to Michelson, Tezos’ approach to smart contract languages with a similar end goal
Current state of development of Scilla, and next milestones
Episode links:
Our previous episode on the Zilliqa platform
Ilya Sergey's paper on mechanising blockchain consensus
Scilla whitepaper
Michelson, Tezos platform's smart contract language
Zilliqa blog for updates on platform development
Coq, a formal proof management system
This episode is hosted by Meher Roy and Sunny Aggarwal. Show notes and listening options: epicenter.tv/238
Scilla is a Turing incomplete intermediate level language; inspired from the paradigms of functional programming and formal verification; that makes it easy for smart contract developers to automatically prove statements about smart contract behavior. For example, Scilla could allow a future multi-signature smart contract author to mathematically prove that funds in that contract would always be retrievable by certain addresses (and never get stuck like the Parity incident). The ability to mathematically prove such safety properties of the smart contract has the potential to be an enabling invention prior to widescale use of this technology.
In this episode, we are joined by Dr. Amrit Kumar and Dr. Ilya Sergey to discuss Scilla, the smart contract language of the upcoming Zilliqa blockchain. In a previous episode, we’ve already covered the vision and technical approach of Zilliqa to solve the transaction scalability problem of permissionless blockchains. This episode focuses specifically on their smart contract language development efforts.
Topics covered in this episode:
Updated on Zilliqa’s progress since our last episode
The technology of mechanised proofs
Dr. Ilya Serger’s effort to mechanically prove safety properties of a blockchain consensus network
Aims of the Scilla language
Future capabilities enabled by the Scilla language
Developer experience and perspective using formal verification tools
How Scilla compares to Michelson, Tezos’ approach to smart contract languages with a similar end goal
Current state of development of Scilla, and next milestones
Episode links:
Our previous episode on the Zilliqa platform
Ilya Sergey's paper on mechanising blockchain consensus
Scilla whitepaper
Michelson, Tezos platform's smart contract language
Zilliqa blog for updates on platform development
Coq, a formal proof management system
This episode is hosted by Meher Roy and Sunny Aggarwal. Show notes and listening options: epicenter.tv/238
Released:
Jun 6, 2018
Format:
Podcast episode
Titles in the series (100)
Jorge Timon & Mark Friedenbach: Bitcoin 2014, Freicoin, Freimarkets & Sidechains: We recorded episode 20 in Amsterdam the morning after the Bitcoin 2014 conference organized by the Bitcoin Foundation. Our two guests for the post-conference sit-down were Jorge Timon and Mark Friedenbach. Jorge is the founder of Freicoin, which is, from an economic perspective, one of the most innovative altcoins. They are also the creators of Freimarkets, which aims to bring Bitcoin 2.0 capabilities into the Bitcoin feature set itself. Finally, they are part of the newly formed Blockstream company, which will develop the Sidechains proposal. by Epicenter - Learn about Crypto, Blockchain, Ethereum, Bitcoin and Distributed Technologies