{"id":5521,"date":"2019-05-03T02:27:43","date_gmt":"2019-05-03T02:27:43","guid":{"rendered":"http:\/\/thebitcoinpodcast.com\/?p=5521"},"modified":"2019-05-03T02:27:43","modified_gmt":"2019-05-03T02:27:43","slug":"hashing-it-out-44","status":"publish","type":"post","link":"https:\/\/thebitcoinpodcast.com\/hashing-it-out-44\/","title":{"rendered":"Hashing It Out #44: Blockstream &#8211; Russell O&#8217;Connor"},"content":{"rendered":"<p><iframe loading=\"lazy\" src=\"https:\/\/player.simplecast.com\/e919dd60-50bd-4ed5-9ad7-1186bb222515?dark=true\" width=\"100%\" height=\"200px\" frameborder=\"no\" scrolling=\"no\" seamless=\"\"><\/iframe><\/p>\n<p>We bring you another brilliant mind on the show for this episode! Russell O&#8217;Connor, developer of Blockstream&#8217;s Simplicity programming language for Bitcoin, dives deep into formal verification topics. We learn about the language design principles driving Simplicity, how formal verification plays an integral role in making the language suitable for securely automating Bitcoin transactions, and the challenges in creating a smart contract script for Bitcoin. We get a glimpse into the future of blockchain automation, and he elucidates what is being done right and what could be done better in blockchain platforms to place security first in smart contract design.<\/p>\n<p><strong>Links:<\/strong><br \/>\n<a href=\"https:\/\/github.com\/ElementsProject\/simplicity\" target=\"_blank\" rel=\"nofollow noopener noreferrer\">Simplicity&#8217;s Github<\/a><br \/>\n<a href=\"https:\/\/arxiv.org\/abs\/1711.03028\" target=\"_blank\" rel=\"nofollow noopener noreferrer\">Simplicity Publication &#8212; PLAS 2017<\/a><br \/>\n<a href=\"https:\/\/youtu.be\/VOeUq3oR2fk\" target=\"_blank\" rel=\"nofollow noopener noreferrer\">Simplicity presentation &#8212; BPASE 2018<\/a> (<a href=\"https:\/\/cyber.stanford.edu\/sites\/g\/files\/sbiybj9936\/f\/slides-bpase-2018.pdf\" target=\"_blank\" rel=\"nofollow noopener noreferrer\">slides<\/a>)<br \/>\n<a href=\"https:\/\/www.youtube.com\/watch?v=M4XnDrRIKx8\" target=\"_blank\" rel=\"nofollow noopener noreferrer\">Illustration of formal verification using Simplicity &#8212; Scale by the Bay 2018<\/a> (<a href=\"https:\/\/lists.ozlabs.org\/pipermail\/simplicity\/2018\/000011.html\" target=\"_blank\" rel=\"nofollow noopener noreferrer\">slides<\/a>)<br \/>\n<a href=\"https:\/\/fc17.ifca.ai\/bitcoin\/papers\/bitcoin17-final28.pdf\" target=\"_blank\" rel=\"nofollow noopener noreferrer\">Enhancing Bitcoin Transactions with Covenants &#8212; The Financial Crypography 2017 Workshop<\/a><br \/>\n<a href=\"https:\/\/vst.cs.princeton.edu\/\" target=\"_blank\" rel=\"nofollow noopener noreferrer\">Andrew Appel&#8217;s Verified Software Toolchain for formal verification of C<\/a><br \/>\n<a href=\"https:\/\/coq.inria.fr\/\" target=\"_blank\" rel=\"nofollow noopener noreferrer\">The Coq proof assistant<\/a><br \/>\n<a href=\"https:\/\/www.cs.tau.ac.il\/~odedp\/modularity-for-decidability.pdf\" target=\"_blank\" rel=\"nofollow noopener noreferrer\">Mooly Sagiv&#8217;s Modularity for Decidability: Implementing and Semi-Automatically Verifying Distributed Systems<\/a><\/p>\n<p>&nbsp;<\/p>\n","protected":false},"excerpt":{"rendered":"<p>We bring you another brilliant mind on the show for this episode! Russell O&#8217;Connor, developer of Blockstream&#8217;s Simplicity programming language for Bitcoin, dives deep into formal verification topics. We learn about the language design principles driving Simplicity, how formal verification plays an integral role in making the language suitable for securely automating Bitcoin transactions, and [&hellip;]<\/p>\n","protected":false},"author":3,"featured_media":5522,"comment_status":"open","ping_status":"open","sticky":false,"template":"","format":"standard","meta":{"nf_dc_page":"","unlock_protocol_post_locks":"","publish_to_discourse":"","publish_post_category":"","wpdc_auto_publish_overridden":"","wpdc_topic_tags":"","wpdc_pin_topic":"","wpdc_pin_until":"","discourse_post_id":"","discourse_permalink":"","wpdc_publishing_response":"","wpdc_publishing_error":"","footnotes":""},"categories":[99],"tags":[],"_links":{"self":[{"href":"https:\/\/thebitcoinpodcast.com\/wp-json\/wp\/v2\/posts\/5521"}],"collection":[{"href":"https:\/\/thebitcoinpodcast.com\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/thebitcoinpodcast.com\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/thebitcoinpodcast.com\/wp-json\/wp\/v2\/users\/3"}],"replies":[{"embeddable":true,"href":"https:\/\/thebitcoinpodcast.com\/wp-json\/wp\/v2\/comments?post=5521"}],"version-history":[{"count":1,"href":"https:\/\/thebitcoinpodcast.com\/wp-json\/wp\/v2\/posts\/5521\/revisions"}],"predecessor-version":[{"id":5523,"href":"https:\/\/thebitcoinpodcast.com\/wp-json\/wp\/v2\/posts\/5521\/revisions\/5523"}],"wp:featuredmedia":[{"embeddable":true,"href":"https:\/\/thebitcoinpodcast.com\/wp-json\/wp\/v2\/media\/5522"}],"wp:attachment":[{"href":"https:\/\/thebitcoinpodcast.com\/wp-json\/wp\/v2\/media?parent=5521"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/thebitcoinpodcast.com\/wp-json\/wp\/v2\/categories?post=5521"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/thebitcoinpodcast.com\/wp-json\/wp\/v2\/tags?post=5521"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}