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 complete 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 discussed in this episode:Updated on Zilliqa's progress since our last episodeThe technology of mechanised proofsDr. Ilya Serger's effort to mechanically prove safety properties of a blockchain consensus networkAims of the Scilla languageFuture capabilities enabled by the Scilla languageDeveloper experience and perspective using formal verification toolsHow Scilla compares to Michelson, Tezos' approach to smart contract languages with a similar end goalCurrent state of development of Scilla, and next milestones Links mentioned in this episode: Our previous episode on the Zilliqa platformIlya Sergey's paper on mechanising blockchain consensusScilla whitepaperMichelson, Tezos platform's smart contract languageZilliqa blog for updates on platform developmentCoq, a formal proof management system Sponsors: Gnosis X: Build a revolutionary prediction market dApp on Gnosis & win up to '$100,000 in GNO tokens Support the show, consider donating: BTC: 1CD83r9EzFinDNWwmRW4ssgCbhsM5bxXwg (https://epicenter.tv/tipbtc)BCC: 1M4dvWxjL5N9WniNtatKtxW7RcGV73TQTd (http://epicenter.tv/tipbch)ETH: 0x8cdb49ca5103Ce06717C4daBBFD4857183f50935 (https://epicenter.tv/tipeth) This episode is also available on :Epicenter.tvYouTubeSouncloud Watch or listen, Epicenter is available wherever you get your podcasts. Epicenter is hosted by Brian Fabian Crain, Sƒbastien Couture & Meher Roy.